TransfinitePropagator.lean

1import BFPP.ProfileRestriction2import BFPP.PrefixFactorization34/-! # Transfinite contractive propagators -/56namespace BFPP78set_option autoImplicit false9open Set Order1011universe u12variable {κ : Ordinal.{u}}1314noncomputable def inputPrefix (D : Set (BoundedFamily (OrdinalIndex κ))) (i : OrdinalIndex κ)15    (x : D) : BoundedFamily (OrdinalIndex i.val) := restrictFamily i.property.le x.val1617noncomputable def prefixLift (D : Set (BoundedFamily (OrdinalIndex κ))) (i : OrdinalIndex κ)18    (x : D) : range (inputPrefix D i) := ⟨inputPrefix D i x, mem_range_self x⟩1920/-- The successor rules are defined on exactly the prefixes arising from the domain.21The sign of the envelope at each limit is fixed independently of the input. -/22structure IsTCP (D : Set (BoundedFamily (OrdinalIndex κ))) (P : D → D) : Prop where23  positive : 0 < κ24  nonempty : D.Nonempty25  at_zero : ∃ c : ℝ, ∀ x, (P x).val ⟨0, positive⟩ = c26  successor_rules : ∀ i : OrdinalIndex κ, i.val ∈ range (Order.succ : Ordinal.{u} → Ordinal.{u}) →27    ∃ Φ : range (inputPrefix D i) → ℝ, LipschitzWith 1 Φ ∧28      ∀ x, Φ (prefixLift D i x) = (P x).val i29  limit_rules : ∀ i : OrdinalIndex κ, IsSuccLimit i.val →30    ∃ ε : Bool, ∀ x, (P x).val i =31      if ε then upperEnvelope (inputPrefix D i x) else lowerEnvelope (inputPrefix D i x)3233theorem inputPrefix_dist_le (D : Set (BoundedFamily (OrdinalIndex κ))) (i : OrdinalIndex κ)34    (x y : D) : dist (inputPrefix D i x) (inputPrefix D i y) ≤ dist x y := by35  change dist (restrictFamily i.property.le x.val) (restrictFamily i.property.le y.val) ≤36    dist x.val y.val37  simpa only [NNReal.coe_one, one_mul] using38    (restrictFamily_nonexpansive i.property.le).dist_le_mul x.val y.val3940theorem IsTCP.nonexpansive {D : Set (BoundedFamily (OrdinalIndex κ))} {P : D → D}41    (h : IsTCP D P) : LipschitzWith 1 P := by42  apply LipschitzWith.of_dist_le_mul43  intro x y44  simp only [NNReal.coe_one, one_mul]45  change dist (P x).val (P y).val ≤ dist x y46  apply (BoundedFamily.dist_le_iff _ _ dist_nonneg).mpr47  intro i48  rcases Ordinal.zero_or_succ_or_isSuccLimit i.val with hi | hi | hi49  · obtain ⟨c, hc⟩ := h.at_zero50    have he : i = ⟨0, h.positive⟩ := Subtype.ext hi51    rw [he, hc x, hc y, sub_self, abs_zero]52    exact dist_nonneg53  · obtain ⟨Φ, hΦ, hΦeq⟩ := h.successor_rules i hi54    have hh := hΦ.dist_le_mul (prefixLift D i x) (prefixLift D i y)55    have hb : |(P x).val i - (P y).val i| ≤ dist (inputPrefix D i x) (inputPrefix D i y) := by56      change |(P x).val i - (P y).val i| ≤ dist (prefixLift D i x) (prefixLift D i y)57      simpa only [NNReal.coe_one, one_mul, hΦeq, Real.dist_eq] using hh58    exact hb.trans (inputPrefix_dist_le D i x y)59  · letI : Nonempty (OrdinalIndex i.val) := ⟨⟨0, hi.pos⟩⟩60    obtain ⟨ε, hε⟩ := h.limit_rules i hi61    have hb : |(P x).val i - (P y).val i| ≤ dist (inputPrefix D i x) (inputPrefix D i y) := by62      rw [hε x, hε y]63      cases ε64      · simpa only [Bool.false_eq_true, ite_false, NNReal.coe_one, one_mul, Real.dist_eq] using65          lowerEnvelope_nonexpansive.dist_le_mul (inputPrefix D i x) (inputPrefix D i y)66      · simpa only [ite_true, NNReal.coe_one, one_mul, Real.dist_eq] using67          upperEnvelope_nonexpansive.dist_le_mul (inputPrefix D i x) (inputPrefix D i y)68    exact hb.trans (inputPrefix_dist_le D i x y)6970theorem isTCP_of_causal {D : Set (BoundedFamily (OrdinalIndex κ))} (P : D → D)71    (hpos : 0 < κ) (hne : D.Nonempty) (c : ℝ) (hzero : ∀ x, (P x).val ⟨0, hpos⟩ = c)72    (hcausal : ∀ i x y, dist ((P x).val i) ((P y).val i) ≤73      dist (inputPrefix D i x) (inputPrefix D i y))74    (hlimit : ∀ i, IsSuccLimit i.val → ∀ x,75      (P x).val i = lowerEnvelope (inputPrefix D i x)) : IsTCP D P := by76  refine ⟨hpos, hne, ⟨c, hzero⟩, ?_, ?_⟩77  · intro i _78    exact exists_nonexpansive_factor (fun x => (P x).val i) (inputPrefix D i) (hcausal i)79  · intro i hi80    exact ⟨false, fun x => hlimit i hi x⟩8182end BFPP

SHA-256