CubicPathwidth.T2.IdealLimit

Source file CubicPathwidth/T2/IdealLimit.lean of the Lean project (how it is built).

import CubicPathwidth.T2.Defs
import CubicPathwidth.C3.GaussianTools

/-!
# Continuity of the ideal 4-star supremum (O7), conditional on the bridge

`idealLimit_of_bridge` is conditional on `BridgeClaim`. We use the bridge only
to write `idealStarFn 4 r τ` as the standard-Gaussian probability of a
frontier event for explicit vectors `wv r : Fin 5 → Sample 4` whose Gram
matrix is `idealStarCov 4 r`. A Chebyshev plus anti-concentration estimate
then bounds the change in `r`, uniformly in `τ`.
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory Filter Topology

namespace CubicPathwidth
namespace T2

abbrev S4 := GaussianField.Sample 4

/-- `c r = √((1 - r²)/3)`. -/
def cc (r : ℝ) : ℝ := Real.sqrt ((1 - r ^ 2) / 3)

/-- Explicit vectors realizing the ideal 4-star: the center `e₀` and
`r e₀ + √(1-r²) u_i` with `u_i` the tetrahedral unit vectors in coordinates 1..3. -/
def wv (r : ℝ) : Fin 5 → S4
  | 0 => !₂[1, 0, 0, 0]
  | 1 => !₂[r, cc r, cc r, cc r]
  | 2 => !₂[r, cc r, -cc r, -cc r]
  | 3 => !₂[r, -cc r, cc r, -cc r]
  | 4 => !₂[r, -cc r, -cc r, cc r]

theorem cc_sq {r : ℝ} (h : r ≤ 1) (h0 : 0 ≤ r) : cc r ^ 2 = (1 - r ^ 2) / 3 := by
  unfold cc
  rw [Real.sq_sqrt]
  have : r ^ 2 ≤ 1 := by nlinarith
  linarith

theorem inner_s4 (x y : S4) :
    ⟪x, y⟫ = x 0 * y 0 + x 1 * y 1 + x 2 * y 2 + x 3 * y 3 := by
  simp [PiLp.inner_apply, Fin.sum_univ_four, mul_comm]

theorem gram_wv {r : ℝ} (h0 : 0 ≤ r) (h1 : r ≤ 1) : gram (wv r) = idealStarCov 4 r := by
  have hc := cc_sq h1 h0
  ext i j
  simp only [gram]
  rw [inner_s4]
  fin_cases i <;> fin_cases j <;>
    simp [idealStarCov, wv] <;> nlinarith [hc]

theorem norm_wv {r : ℝ} (h0 : 0 ≤ r) (h1 : r ≤ 1) (i : Fin 5) : ‖wv r i‖ = 1 := by
  have h : ⟪wv r i, wv r i⟫ = 1 := by
    have := congrFun (congrFun (gram_wv h0 h1) i) i
    simpa [gram, idealStarCov] using this
  rw [real_inner_self_eq_norm_sq] at h
  have hn : 0 ≤ ‖wv r i‖ := norm_nonneg _
  nlinarith

theorem cc_sub_sq {r r' : ℝ} (h0 : 0 ≤ r) (h1 : r ≤ 1) (h0' : 0 ≤ r') (h1' : r' ≤ 1) :
    (cc r' - cc r) ^ 2 ≤ 2 / 3 * |r' - r| := by
  have hc := cc_sq h1 h0
  have hc' := cc_sq h1' h0'
  have a0 : 0 ≤ cc r := Real.sqrt_nonneg _
  have a0' : 0 ≤ cc r' := Real.sqrt_nonneg _
  have key : |cc r' ^ 2 - cc r ^ 2| ≤ 2 / 3 * |r' - r| := by
    rw [hc, hc']
    have : (1 - r' ^ 2) / 3 - (1 - r ^ 2) / 3 = -((r' - r) * (r' + r)) / 3 := by ring
    rw [this, abs_div, abs_neg, abs_mul]
    have : |r' + r| ≤ 2 := by rw [abs_le]; constructor <;> linarith
    have h3 : (3 : ℝ) = |(3 : ℝ)| := by norm_num
    rw [← h3]
    have := mul_le_mul_of_nonneg_left this (abs_nonneg (r' - r))
    rw [div_le_iff₀ (by norm_num)]
    linarith
  calc (cc r' - cc r) ^ 2 = |cc r' - cc r| * |cc r' - cc r| := by rw [← sq, sq_abs]
    _ ≤ |cc r' - cc r| * |cc r' + cc r| := by
        apply mul_le_mul_of_nonneg_left _ (abs_nonneg _)
        rw [abs_of_nonneg (by linarith : 0 ≤ cc r' + cc r)]
        rw [abs_le]; constructor <;> linarith
    _ = |cc r' ^ 2 - cc r ^ 2| := by rw [← abs_mul]; ring_nf
    _ ≤ _ := key

theorem norm_sub_wv_sq {r r' : ℝ} (h0 : 0 ≤ r) (h1 : r ≤ 1) (h0' : 0 ≤ r') (h1' : r' ≤ 1)
    (i : Fin 5) : ‖wv r' i - wv r i‖ ^ 2 ≤ 3 * |r' - r| := by
  have hcc := cc_sub_sq h0 h1 h0' h1'
  have hη : |r' - r| ≤ 1 := by rw [abs_le]; constructor <;> linarith
  have hsq : (r' - r) ^ 2 ≤ |r' - r| := by
    rw [← sq_abs]
    nlinarith [abs_nonneg (r' - r)]
  rw [← real_inner_self_eq_norm_sq, inner_s4]
  fin_cases i <;> simp [wv] <;> nlinarith [abs_nonneg (r' - r)]

/-- Chebyshev for a linear form. -/
theorem cheb_inner (d : S4) {δ : ℝ} (hδ : 0 < δ) :
    (stdGaussian S4).real {x | δ ≤ |⟪d, x⟫|} ≤ ‖d‖ ^ 2 / δ ^ 2 := by
  by_cases hd : d = 0
  · subst hd
    have : {x : S4 | δ ≤ |⟪(0 : S4), x⟫|} = ∅ := by
      ext x; simp; exact hδ
    rw [this]; simp
  · have hn : 0 < ‖d‖ := norm_pos_iff.mpr hd
    set a : S4 := ‖d‖⁻¹ • d with ha_def
    have ha : ‖a‖ = 1 := by
      rw [ha_def, norm_smul, norm_inv, norm_norm, inv_mul_cancel₀ hn.ne']
    have hset : {x : S4 | δ ≤ |⟪d, x⟫|} = {x : S4 | ⟪a, x⟫ ∈ {y : ℝ | δ / ‖d‖ ≤ |y|}} := by
      ext x
      have : ⟪d, x⟫ = ‖d‖ * ⟪a, x⟫ := by
        rw [ha_def, real_inner_smul_left, ← mul_assoc, mul_inv_cancel₀ hn.ne', one_mul]
      simp only [Set.mem_ofPred_eq, this, abs_mul, abs_of_pos hn]
      rw [div_le_iff₀ hn, mul_comm]
    rw [hset, C3.real_unit_projection ha (measurableSet_le measurable_const (by fun_prop))]
    have := C3.gaussianReal_abs_ge_le (div_pos hδ hn)
    refine this.trans (le_of_eq ?_)
    field_simp

/-- The key one-leaf estimate. -/
theorem leaf_bound (a a' : S4) (ha : ‖a‖ = 1) {δ : ℝ} (hδ : 0 < δ) (τ : ℝ) :
    (stdGaussian S4).real {x | ⟪a, x⟫ ≤ τ ∧ τ < ⟪a', x⟫} ≤ ‖a' - a‖ ^ 2 / δ ^ 2 + δ / 2 := by
  have hsub : {x : S4 | ⟪a, x⟫ ≤ τ ∧ τ < ⟪a', x⟫} ⊆
      {x | δ ≤ |⟪a' - a, x⟫|} ∪ {x | ⟪a, x⟫ ∈ Set.Ioc (τ - δ) τ} := by
    intro x ⟨h1, h2⟩
    by_cases h : δ ≤ |⟪a' - a, x⟫|
    · exact Or.inl h
    · right
      push Not at h
      rw [inner_sub_left] at h
      have := (abs_lt.mp h).2
      exact ⟨by linarith, h1⟩
  refine (measureReal_mono hsub).trans ((measureReal_union_le _ _).trans ?_)
  have h1 := cheb_inner (a' - a) hδ
  have h2 : (stdGaussian S4).real {x | ⟪a, x⟫ ∈ Set.Ioc (τ - δ) τ} ≤ δ / 2 := by
    rw [C3.real_unit_projection ha measurableSet_Ioc]
    have := C3.gaussianReal_Ioc_le (a := τ - δ) (b := τ) (by linarith)
    linarith
  linarith

/-- The frontier event for the explicit vectors. -/
def Ev (r τ : ℝ) : Set S4 :=
  {x | τ < ⟪wv r 0, x⟫ ∧ ∃ i : Fin 5, i ≠ 0 ∧ ⟪wv r i, x⟫ ≤ τ}

theorem measurableSet_frontierEvent_IL (τ : ℝ) : MeasurableSet (frontierEvent 4 τ) := by
  have : frontierEvent 4 τ =
      {x : EuclideanSpace ℝ (Fin 5) | τ < x 0} ∩
        ⋃ i : Fin 5, ⋃ (_ : i ≠ 0), {x | x i ≤ τ} := by
    ext x; simp [frontierEvent]
  rw [this]
  refine MeasurableSet.inter (measurableSet_lt measurable_const (by fun_prop))
    (MeasurableSet.iUnion fun i => MeasurableSet.iUnion fun _ =>
      measurableSet_le (by fun_prop) measurable_const)

theorem idealStarFn_eq (hb : BridgeClaim) {r : ℝ} (h0 : 0 ≤ r) (h1 : r ≤ 1) (τ : ℝ) :
    idealStarFn 4 r τ = (stdGaussian S4).real (Ev r τ) := by
  unfold idealStarFn
  rw [← gram_wv h0 h1, hb 4 5 (wv r) _ (measurableSet_frontierEvent_IL τ)]
  rfl

theorem idealStarFn_mem_Icc (hb : BridgeClaim) {r : ℝ} (h0 : 0 ≤ r) (h1 : r ≤ 1) (τ : ℝ) :
    0 ≤ idealStarFn 4 r τ ∧ idealStarFn 4 r τ ≤ 1 := by
  rw [idealStarFn_eq hb h0 h1]
  exact ⟨measureReal_nonneg, measureReal_le_one⟩

/-- One-sided uniform continuity estimate. -/
theorem star_diff_le (hb : BridgeClaim) {r r' : ℝ} (h0 : 0 ≤ r) (h1 : r ≤ 1) (h0' : 0 ≤ r')
    (h1' : r' ≤ 1) {δ : ℝ} (hδ : 0 < δ) (τ : ℝ) :
    idealStarFn 4 r' τ - idealStarFn 4 r τ ≤ 12 * |r' - r| / δ ^ 2 + 2 * δ := by
  rw [idealStarFn_eq hb h0 h1, idealStarFn_eq hb h0' h1']
  have hsub : Ev r' τ ⊆ Ev r τ ∪ ⋃ i : Fin 4,
      {x | ⟪wv r' i.succ, x⟫ ≤ τ ∧ τ < ⟪wv r i.succ, x⟫} := by
    intro x ⟨hc, i, hi, hle⟩
    by_cases hx : x ∈ Ev r τ
    · exact Or.inl hx
    · right
      have hc' : τ < ⟪wv r 0, x⟫ := by simpa [wv] using hc
      have : ¬ ⟪wv r i, x⟫ ≤ τ := fun h => hx ⟨hc', i, hi, h⟩
      obtain ⟨j, rfl⟩ := Fin.exists_succ_eq.mpr hi
      exact Set.mem_iUnion.mpr ⟨j, hle, not_le.mp this⟩
  have hA := (measureReal_mono (μ := stdGaussian S4) hsub).trans
    (measureReal_union_le (μ := stdGaussian S4) _ _)
  have hU := measureReal_iUnion_fintype_le (μ := stdGaussian S4)
    (fun i : Fin 4 => {x | ⟪wv r' i.succ, x⟫ ≤ τ ∧ τ < ⟪wv r i.succ, x⟫})
  have hleaf : ∀ i : Fin 4,
      (stdGaussian S4).real {x | ⟪wv r' i.succ, x⟫ ≤ τ ∧ τ < ⟪wv r i.succ, x⟫} ≤
        3 * |r' - r| / δ ^ 2 + δ / 2 := by
    intro i
    refine (leaf_bound _ _ (norm_wv h0' h1' _) hδ τ).trans ?_
    have := norm_sub_wv_sq h0' h1' h0 h1 i.succ
    rw [abs_sub_comm] at this
    have h3 : ‖wv r i.succ - wv r' i.succ‖ ^ 2 / δ ^ 2 ≤ 3 * |r' - r| / δ ^ 2 := by
      apply div_le_div_of_nonneg_right _ (by positivity)
      exact this
    linarith
  rw [Fin.sum_univ_four] at hU
  have := hleaf 0
  have := hleaf 1
  have := hleaf 2
  have := hleaf 3
  have e : 12 * |r' - r| / δ ^ 2 = 4 * (3 * |r' - r| / δ ^ 2) := by ring
  linarith

theorem star_abs_le (hb : BridgeClaim) {r r' : ℝ} (h0 : 0 ≤ r) (h1 : r ≤ 1) (h0' : 0 ≤ r')
    (h1' : r' ≤ 1) {δ : ℝ} (hδ : 0 < δ) (τ : ℝ) :
    |idealStarFn 4 r' τ - idealStarFn 4 r τ| ≤ 12 * |r' - r| / δ ^ 2 + 2 * δ := by
  rw [abs_le]
  constructor
  · have := star_diff_le hb h0' h1' h0 h1 hδ τ
    rw [abs_sub_comm] at this
    linarith
  · exact star_diff_le hb h0 h1 h0' h1' hδ τ

theorem idealSup_close (hb : BridgeClaim) {r r' : ℝ} (h0 : 0 ≤ r) (h1 : r ≤ 1) (h0' : 0 ≤ r')
    (h1' : r' ≤ 1) {B : ℝ} (hB : ∀ τ, |idealStarFn 4 r' τ - idealStarFn 4 r τ| ≤ B) :
    |idealSup r' - idealSup r| ≤ B := by
  have bdd : ∀ {s : ℝ}, 0 ≤ s → s ≤ 1 → BddAbove (Set.range fun τ : ℝ => idealStarFn 4 s τ) :=
    fun hs0 hs1 => ⟨1, by rintro _ ⟨τ, rfl⟩; exact (idealStarFn_mem_Icc hb hs0 hs1 τ).2⟩
  have one_side : ∀ {s s' : ℝ}, 0 ≤ s → s ≤ 1 → 0 ≤ s' → s' ≤ 1 →
      (∀ τ, idealStarFn 4 s' τ - idealStarFn 4 s τ ≤ B) → idealSup s' ≤ idealSup s + B := by
    intro s s' hs0 hs1 hs0' hs1' h
    apply csSup_le (Set.range_nonempty _)
    rintro _ ⟨τ, rfl⟩
    have h2 : idealStarFn 4 s τ ≤ idealSup s := le_csSup (bdd hs0 hs1) ⟨τ, rfl⟩
    have := h τ
    show idealStarFn 4 s' τ ≤ _
    linarith
  rw [abs_le]
  constructor
  · have := one_side h0' h1' h0 h1 (fun τ => by
      have := hB τ; rw [abs_sub_comm] at this; exact (abs_le.mp this).2)
    linarith
  · have := one_side h0 h1 h0' h1' (fun τ => (abs_le.mp (hB τ)).2)
    linarith

theorem r44_mem : 0 ≤ r44 ∧ r44 ≤ 1 := by
  unfold r44
  have h3 : Real.sqrt 3 ^ 2 = 3 := Real.sq_sqrt (by norm_num)
  have h0 : 0 ≤ Real.sqrt 3 := Real.sqrt_nonneg _
  constructor
  · positivity
  · nlinarith

theorem radiusCorr4_mem (R : ℕ) : 0 ≤ radiusCorr4 R ∧ radiusCorr4 R ≤ 1 := by
  obtain ⟨a, b⟩ := r44_mem
  have h1 : 0 ≤ 1 / (R : ℝ) := by positivity
  have h2 : 1 / (R : ℝ) ≤ 1 := by
    rcases Nat.eq_zero_or_pos R with h | h
    · subst h; simp
    · rw [div_le_one (by exact_mod_cast h)]; exact_mod_cast h
  unfold radiusCorr4
  constructor
  · exact mul_nonneg a (by linarith)
  · nlinarith

theorem idealLimit_of_bridge (hb : BridgeClaim) : IdealLimitClaim := by
  rw [IdealLimitClaim, ← idealSup_r44, Metric.tendsto_atTop]
  intro ε hε
  obtain ⟨N, hN⟩ := exists_nat_gt (1536 / ε ^ 3)
  refine ⟨N, fun R hR => ?_⟩
  obtain ⟨m0, m1⟩ := r44_mem
  obtain ⟨c0, c1⟩ := radiusCorr4_mem R
  have hNpos : (0 : ℝ) < N := lt_of_le_of_lt (by positivity) hN
  have hRpos : (0 : ℝ) < R := lt_of_lt_of_le hNpos (by exact_mod_cast hR)
  have hRN : (N : ℝ) ≤ R := by exact_mod_cast hR
  set δ := ε / 8 with hδ
  have hδ0 : 0 < δ := by positivity
  -- the radius gap
  have hgap : |radiusCorr4 R - r44| ≤ 1 / (R : ℝ) := by
    have : radiusCorr4 R - r44 = -(r44 * (1 / (R : ℝ))) := by unfold radiusCorr4; ring
    rw [this, abs_neg, abs_of_nonneg (by positivity)]
    calc r44 * (1 / (R : ℝ)) ≤ 1 * (1 / (R : ℝ)) :=
          mul_le_mul_of_nonneg_right m1 (by positivity)
      _ = 1 / (R : ℝ) := one_mul _
  have hε3 : 0 < ε ^ 3 := by positivity
  have hinv : 1 / (R : ℝ) < ε ^ 3 / 1536 := by
    have h1536 : 1536 / ε ^ 3 < (R : ℝ) := lt_of_lt_of_le hN hRN
    rw [div_lt_iff₀ hε3] at h1536
    rw [div_lt_div_iff₀ hRpos (by norm_num)]
    linarith
  have hB := idealSup_close hb m0 m1 c0 c1
    (B := 12 * |radiusCorr4 R - r44| / δ ^ 2 + 2 * δ)
    (fun τ => star_abs_le hb m0 m1 c0 c1 hδ0 τ)
  rw [Real.dist_eq]
  refine lt_of_le_of_lt hB ?_
  have hδsq : δ ^ 2 = ε ^ 2 / 64 := by rw [hδ]; ring
  have : 12 * |radiusCorr4 R - r44| / δ ^ 2 ≤ ε / 2 := by
    rw [div_le_iff₀ (by positivity), hδsq]
    have : |radiusCorr4 R - r44| ≤ ε ^ 3 / 1536 := (hgap.trans hinv.le)
    nlinarith [this]
  have h2δ : 2 * δ = ε / 4 := by rw [hδ]; ring
  linarith

end T2
end CubicPathwidth

#print axioms CubicPathwidth.T2.idealLimit_of_bridge