EncodedMaps.lean

1import BFPP.EncodedDomain23/-! # Analysis, synthesis, and propagation on the encoded domain -/45namespace BFPP67set_option autoImplicit false8open Order910universe u v11variable {ρ σ κ : Ordinal.{u}} [Fact (IsSuccLimit ρ)] [Fact (IsSuccLimit σ)] [Fact (IsSuccLimit κ)]1213noncomputable def encodedPropagator (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ) :14    EncodedDomain hρκ hσκ → EncodedDomain hρκ hσκ :=15  fun x => encodeIso hρκ hσκ ((encodeIso hρκ hσκ).symm x).delay1617@[simp] theorem encodedPropagator_encode (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)18    (z : TwoProfile (OrdinalIndex ρ) (OrdinalIndex σ)) :19    encodedPropagator hρκ hσκ (encodeIso hρκ hσκ z) = encodeIso hρκ hσκ z.delay := by20  simp only [encodedPropagator, IsometryEquiv.symm_apply_apply]2122theorem encodedPropagator_nonexpansive (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ) :23    LipschitzWith 1 (encodedPropagator hρκ hσκ) := by24  apply LipschitzWith.of_dist_le_mul25  intro x y26  simp only [NNReal.coe_one, one_mul]27  change dist (encodeIso hρκ hσκ ((encodeIso hρκ hσκ).symm x).delay)28    (encodeIso hρκ hσκ ((encodeIso hρκ hσκ).symm y).delay) ≤ dist x y29  rw [(encodeIso hρκ hσκ).dist_eq]30  have h := TwoProfile.delay_nonexpansive.dist_le_mul31    ((encodeIso hρκ hσκ).symm x) ((encodeIso hρκ hσκ).symm y)32  simpa only [NNReal.coe_one, one_mul, (encodeIso hρκ hσκ).symm.dist_eq] using h3334variable {K : Type v} [TopologicalSpace K] [CompactSpace K]3536noncomputable def encodedAnalysis (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)37    (F : InseparablePair K (OrdinalIndex ρ) (OrdinalIndex σ)) :38    UnitBall C(K, ℝ) → EncodedDomain hρκ hσκ :=39  fun f => encodeIso hρκ hσκ (F.levels.analyze f)4041noncomputable def encodedSynthesis (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)42    (F : InseparablePair K (OrdinalIndex ρ) (OrdinalIndex σ)) :43    EncodedDomain hρκ hσκ → UnitBall C(K, ℝ) :=44  fun x => F.synthesize ((encodeIso hρκ hσκ).symm x)4546theorem encodedAnalysis_nonexpansive (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)47    (F : InseparablePair K (OrdinalIndex ρ) (OrdinalIndex σ)) :48    LipschitzWith 1 (encodedAnalysis hρκ hσκ F) := by49  apply LipschitzWith.of_dist_le_mul50  intro f g51  simp only [NNReal.coe_one, one_mul]52  change dist (encodeIso hρκ hσκ (F.levels.analyze f))53    (encodeIso hρκ hσκ (F.levels.analyze g)) ≤ dist f g54  rw [(encodeIso hρκ hσκ).dist_eq]55  simpa only [NNReal.coe_one, one_mul] using F.levels.analyze_nonexpansive.dist_le_mul f g5657theorem encodedSynthesis_nonexpansive (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)58    (F : InseparablePair K (OrdinalIndex ρ) (OrdinalIndex σ)) :59    LipschitzWith 1 (encodedSynthesis hρκ hσκ F) := by60  apply LipschitzWith.of_dist_le_mul61  intro x y62  simp only [NNReal.coe_one, one_mul]63  have h := F.synthesize_nonexpansive.dist_le_mul ((encodeIso hρκ hσκ).symm x)64    ((encodeIso hρκ hσκ).symm y)65  simpa only [NNReal.coe_one, one_mul, (encodeIso hρκ hσκ).symm.dist_eq, encodedSynthesis] using h6667theorem encoded_coefficient_fixedPointFree (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)68    (F : InseparablePair K (OrdinalIndex ρ) (OrdinalIndex σ)) (x : EncodedDomain hρκ hσκ) :69    encodedAnalysis hρκ hσκ F (encodedSynthesis hρκ hσκ F (encodedPropagator hρκ hσκ x)) ≠ x := by70  intro he71  have he' := congrArg (encodeIso hρκ hσκ).symm he72  have hc : F.levels.analyze (F.synthesize ((encodeIso hρκ hσκ).symm x).delay) =73      (encodeIso hρκ hσκ).symm x := by74    simpa only [encodedAnalysis, encodedSynthesis, encodedPropagator,75      IsometryEquiv.symm_apply_apply] using he'76  have hle := F.analyze_synthesize_le ((encodeIso hρκ hσκ).symm x).delay77  rw [hc] at hle78  exact TwoProfile.no_subsolution _ hle7980theorem encoded_ballMap_eq (hρκ : ρ ≤ κ) (hσκ : σ ≤ κ)81    (F : InseparablePair K (OrdinalIndex ρ) (OrdinalIndex σ)) :82    (fun f => encodedSynthesis hρκ hσκ F (encodedPropagator hρκ hσκ (encodedAnalysis hρκ hσκ F f))) =83      F.ballMap := by84  funext f85  simp only [encodedAnalysis, encodedSynthesis, encodedPropagator,86    IsometryEquiv.symm_apply_apply, InseparablePair.ballMap]8788end BFPP

SHA-256