CubicPathwidth.T2.StarBoundCont

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

import CubicPathwidth.T2.DefsB
import CubicPathwidth.T2.Bridge
import CubicPathwidth.C3.GaussianTools

/-!
# Continuity of the star bound in the floors (B2)

* `pMin` is Lipschitz in the thresholds: `|pMin a - pMin a'| ≤ ∑ |a i - a' i| / 2`.
* The thresholds `(τ - ρ z)/√(1-ρ²)` are Lipschitz in `ρ`, locally uniformly.
* Integrating against `φ` gives `starBoundCont`.
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory

namespace CubicPathwidth
namespace T2

/-! ## Marginals of a correlation matrix -/

theorem real_marginal_Ioc {m : ℕ} {C : Matrix (Fin m) (Fin m) ℝ} (hC : IsCorrelation C)
    (i : Fin m) (a b : ℝ) :
    (multivariateGaussian 0 C).real {x | x i ∈ Set.Ioc a b} ≤ |b - a| / 2 := by
  rcases le_total a b with hab | hab
  · have h := measurePreserving_eval_multivariateGaussian (μ := 0) hC.1 (i := i)
    have hC1 : (C i i).toNNReal = 1 := by rw [hC.2 i]; simp
    rw [hC1] at h
    have h2 := h.measureReal_preimage (s := Set.Ioc a b) measurableSet_Ioc.nullMeasurableSet
    have h3 : (Set.Ioc a b) = (Set.Ioc a b) := rfl
    simp only [PiLp.zero_apply] at h2
    have : {x : EuclideanSpace ℝ (Fin m) | x i ∈ Set.Ioc a b} =
        (fun x : EuclideanSpace ℝ (Fin m) => x i) ⁻¹' Set.Ioc a b := rfl
    rw [this, h2, abs_of_nonneg (by linarith)]
    exact C3.gaussianReal_Ioc_le hab
  · have : {x : EuclideanSpace ℝ (Fin m) | x i ∈ Set.Ioc a b} = ∅ := by
      ext x; simp only [Set.mem_ofPred_eq, Set.mem_Ioc, Set.mem_empty_iff_false, iff_false, not_and]
      intro h; linarith
    rw [this]; simp; positivity

theorem gaussProb_le_add {m : ℕ} {C : Matrix (Fin m) (Fin m) ℝ} (hC : IsCorrelation C)
    (a a' : Fin m → ℝ) :
    gaussProb C {x | ∀ i, a i < x i} ≤
      gaussProb C {x | ∀ i, a' i < x i} + ∑ i, |a' i - a i| / 2 := by
  set μ := multivariateGaussian (0 : EuclideanSpace ℝ (Fin m)) C
  have hsub : {x : EuclideanSpace ℝ (Fin m) | ∀ i, a i < x i} ⊆
      {x | ∀ i, a' i < x i} ∪ ⋃ i, {x | x i ∈ Set.Ioc (a i) (a' i)} := by
    intro x hx
    by_cases h : ∀ i, a' i < x i
    · exact Or.inl h
    · right
      push Not at h
      obtain ⟨i, hi⟩ := h
      exact Set.mem_iUnion.mpr ⟨i, (hx i), hi⟩
  have h1 : μ.real {x | ∀ i, a i < x i} ≤
      μ.real {x | ∀ i, a' i < x i} + ∑ i, μ.real {x | x i ∈ Set.Ioc (a i) (a' i)} := by
    refine (measureReal_mono hsub).trans ?_
    refine (measureReal_union_le _ _).trans ?_
    gcongr
    exact measureReal_iUnion_fintype_le _
  refine h1.trans ?_
  exact add_le_add le_rfl (Finset.sum_le_sum fun i _ => real_marginal_Ioc hC i _ _)

theorem pMin_nonneg {m : ℕ} (a : Fin m → ℝ) : 0 ≤ pMin a := by
  have : Nonempty {C : Matrix (Fin m) (Fin m) ℝ // IsCorrelation C} :=
    ⟨⟨1, Matrix.PosSemidef.one, by simp⟩⟩
  exact le_ciInf fun C => ENNReal.toReal_nonneg

theorem pMin_le_one {m : ℕ} (a : Fin m → ℝ) : pMin a ≤ 1 := by
  refine (ciInf_le ⟨0, ?_⟩ (⟨1, Matrix.PosSemidef.one, by simp⟩ :
    {C : Matrix (Fin m) (Fin m) ℝ // IsCorrelation C})).trans ?_
  · rintro _ ⟨C, rfl⟩; exact ENNReal.toReal_nonneg
  · exact ENNReal.toReal_le_of_le_ofReal zero_le_one (by
      simpa using prob_le_one (μ := multivariateGaussian 0 (1 : Matrix (Fin m) (Fin m) ℝ)))

theorem pMin_le_add {m : ℕ} (a a' : Fin m → ℝ) :
    pMin a ≤ pMin a' + ∑ i, |a' i - a i| / 2 := by
  have : Nonempty {C : Matrix (Fin m) (Fin m) ℝ // IsCorrelation C} :=
    ⟨⟨1, Matrix.PosSemidef.one, by simp⟩⟩
  have hbdd : BddBelow (Set.range fun C : {C : Matrix (Fin m) (Fin m) ℝ // IsCorrelation C} =>
      gaussProb C.1 {x | ∀ i, a i < x i}) := by
    refine ⟨0, ?_⟩; rintro _ ⟨C, rfl⟩; exact ENNReal.toReal_nonneg
  have : pMin a - ∑ i, |a' i - a i| / 2 ≤ pMin a' := by
    refine le_ciInf fun C => ?_
    have h1 : pMin a ≤ gaussProb C.1 {x | ∀ i, a i < x i} := ciInf_le hbdd C
    have h2 := gaussProb_le_add C.2 a a'
    linarith
  linarith

theorem abs_pMin_sub_le {m : ℕ} (a a' : Fin m → ℝ) :
    |pMin a - pMin a'| ≤ ∑ i, |a i - a' i| / 2 := by
  have h1 := pMin_le_add a a'
  have h2 := pMin_le_add a' a
  have e : ∑ i, |a' i - a i| / 2 = ∑ i, |a i - a' i| / 2 :=
    Finset.sum_congr rfl fun i _ => by rw [abs_sub_comm]
  rw [abs_le]; constructor <;> linarith

theorem continuous_pMin {m : ℕ} : Continuous (pMin : (Fin m → ℝ) → ℝ) := by
  refine (LipschitzWith.of_dist_le_mul (K := (m : NNReal) / 2) fun a a' => ?_).continuous
  rw [Real.dist_eq]
  refine (abs_pMin_sub_le a a').trans ?_
  have : ∀ i, |a i - a' i| / 2 ≤ dist a a' / 2 := fun i => by
    have := dist_le_pi_dist a a' i
    rw [Real.dist_eq] at this
    linarith
  calc ∑ i, |a i - a' i| / 2 ≤ ∑ _i : Fin m, dist a a' / 2 := Finset.sum_le_sum fun i _ => this i
    _ = _ := by simp; ring


/-! ## Lipschitz dependence of the thresholds on the floor -/

/-- The threshold `a_i(z) = (τ - ρ z)/√(1-ρ²)`. -/
def aFun (ρ τ z : ℝ) : ℝ := (τ - ρ * z) / Real.sqrt (1 - ρ ^ 2)

/-- Lipschitz constant of the threshold, given a lower bound `s₀` of the square roots. -/
def lipConst (s₀ : ℝ) : ℝ := 1 / s₀ ^ 3 + (1 / s₀ + 1) / s₀ ^ 2

theorem lipConst_nonneg {s₀ : ℝ} (h : 0 < s₀) : 0 ≤ lipConst s₀ := by
  unfold lipConst; positivity

theorem sqrt_sub_le {ρ ρ' s₀ : ℝ} (hρ : |ρ| ≤ 1) (hρ' : |ρ'| ≤ 1) (hs₀ : 0 < s₀)
    (h1 : s₀ ≤ Real.sqrt (1 - ρ ^ 2)) (h2 : s₀ ≤ Real.sqrt (1 - ρ' ^ 2)) :
    |Real.sqrt (1 - ρ ^ 2) - Real.sqrt (1 - ρ' ^ 2)| ≤ |ρ - ρ'| / s₀ := by
  have hρ2 : ρ ^ 2 ≤ 1 := by nlinarith [abs_le.mp hρ]
  have hρ2' : ρ' ^ 2 ≤ 1 := by nlinarith [abs_le.mp hρ']
  set s := Real.sqrt (1 - ρ ^ 2) with hs
  set s' := Real.sqrt (1 - ρ' ^ 2) with hs'
  have hss : s ^ 2 = 1 - ρ ^ 2 := Real.sq_sqrt (by linarith)
  have hss' : s' ^ 2 = 1 - ρ' ^ 2 := Real.sq_sqrt (by linarith)
  have key : (s - s') * (s + s') = (ρ' - ρ) * (ρ' + ρ) := by linear_combination hss - hss'
  have hpos : 0 < s + s' := by linarith
  have h3 : |s - s'| * (s + s') = |ρ' - ρ| * |ρ' + ρ| := by
    calc |s - s'| * (s + s') = |s - s'| * |s + s'| := by rw [abs_of_pos hpos]
      _ = |(s - s') * (s + s')| := (abs_mul _ _).symm
      _ = _ := by rw [key, abs_mul]
  have h4 : |ρ' + ρ| ≤ 2 := by
    calc |ρ' + ρ| ≤ |ρ'| + |ρ| := abs_add_le _ _
      _ ≤ 2 := by linarith
  have h5 : |s - s'| * (2 * s₀) ≤ |s - s'| * (s + s') :=
    mul_le_mul_of_nonneg_left (by linarith) (abs_nonneg _)
  have h6 : |ρ' - ρ| * |ρ' + ρ| ≤ |ρ' - ρ| * 2 :=
    mul_le_mul_of_nonneg_left h4 (abs_nonneg _)
  rw [abs_sub_comm ρ' ρ] at h6 h3
  rw [le_div_iff₀ hs₀]
  nlinarith

theorem aFun_sub_le {ρ ρ' s₀ : ℝ} (τ z : ℝ) (hρ : |ρ| ≤ 1) (hρ' : |ρ'| ≤ 1) (hs₀ : 0 < s₀)
    (h1 : s₀ ≤ Real.sqrt (1 - ρ ^ 2)) (h2 : s₀ ≤ Real.sqrt (1 - ρ' ^ 2)) :
    |aFun ρ τ z - aFun ρ' τ z| ≤ (|τ| + |z|) * lipConst s₀ * |ρ - ρ'| := by
  have hds := sqrt_sub_le hρ hρ' hs₀ h1 h2
  have hρ2 : ρ ^ 2 ≤ 1 := by nlinarith [abs_le.mp hρ]
  unfold aFun
  set s := Real.sqrt (1 - ρ ^ 2) with hs
  set s' := Real.sqrt (1 - ρ' ^ 2) with hs'
  set D := |ρ - ρ'| with hD
  have hD0 : 0 ≤ D := abs_nonneg _
  have hs1 : s ≤ 1 := Real.sqrt_le_one.mpr (by nlinarith [sq_nonneg ρ]) 
  have hs0 : 0 < s := lt_of_lt_of_le hs₀ h1
  have hs0' : 0 < s' := lt_of_lt_of_le hs₀ h2
  have hss : s₀ ^ 2 ≤ s * s' := by nlinarith
  have hss0 : 0 < s * s' := by positivity
  have hds' : |s' - s| ≤ D / s₀ := by rwa [abs_sub_comm]
  have hX : |1 / s - 1 / s'| ≤ lipConst s₀ * D := by
    have e : 1 / s - 1 / s' = (s' - s) / (s * s') := by field_simp
    rw [e, abs_div, abs_of_pos hss0]
    calc |s' - s| / (s * s') ≤ (D / s₀) / s₀ ^ 2 :=
          div_le_div₀ (by positivity) hds' (by positivity) hss
      _ = D / s₀ ^ 3 := by field_simp
      _ ≤ lipConst s₀ * D := by
          unfold lipConst
          have : 0 ≤ (1 / s₀ + 1) / s₀ ^ 2 := by positivity
          have e2 : D / s₀ ^ 3 = 1 / s₀ ^ 3 * D := by ring
          rw [e2]; nlinarith
  have hY : |ρ / s - ρ' / s'| ≤ lipConst s₀ * D := by
    have e : ρ / s - ρ' / s' = (ρ * (s' - s) + (ρ - ρ') * s) / (s * s') := by field_simp; ring
    rw [e, abs_div, abs_of_pos hss0]
    have hnum : |ρ * (s' - s) + (ρ - ρ') * s| ≤ D / s₀ + D := by
      calc |ρ * (s' - s) + (ρ - ρ') * s| ≤ |ρ * (s' - s)| + |(ρ - ρ') * s| := abs_add_le _ _
        _ = |ρ| * |s' - s| + D * s := by rw [abs_mul, abs_mul, abs_of_pos hs0]
        _ ≤ 1 * (D / s₀) + D * 1 := by
            gcongr
        _ = D / s₀ + D := by ring
    calc |ρ * (s' - s) + (ρ - ρ') * s| / (s * s') ≤ (D / s₀ + D) / s₀ ^ 2 :=
          div_le_div₀ (by positivity) hnum (by positivity) hss
      _ ≤ lipConst s₀ * D := by
          unfold lipConst
          have e2 : (D / s₀ + D) / s₀ ^ 2 = (1 / s₀ + 1) / s₀ ^ 2 * D := by ring
          have : 0 ≤ 1 / s₀ ^ 3 := by positivity
          rw [e2]; nlinarith [mul_nonneg this hD0]
  have e : (τ - ρ * z) / s - (τ - ρ' * z) / s' = τ * (1 / s - 1 / s') - z * (ρ / s - ρ' / s') := by
    ring
  rw [e]
  calc |τ * (1 / s - 1 / s') - z * (ρ / s - ρ' / s')|
      ≤ |τ * (1 / s - 1 / s')| + |z * (ρ / s - ρ' / s')| := abs_sub _ _
    _ = |τ| * |1 / s - 1 / s'| + |z| * |ρ / s - ρ' / s'| := by rw [abs_mul, abs_mul]
    _ ≤ |τ| * (lipConst s₀ * D) + |z| * (lipConst s₀ * D) := by
        gcongr
    _ = (|τ| + |z|) * lipConst s₀ * D := by ring


/-! ## Integrability -/

theorem continuous_phi : Continuous phi := by
  unfold phi; rw [gaussianPDFReal_def]; fun_prop

theorem phi_nonneg (z : ℝ) : 0 ≤ phi z := gaussianPDFReal_nonneg 0 1 z

theorem integrable_phi : Integrable phi := integrable_gaussianPDFReal 0 1

theorem integrable_phi_mul_abs : Integrable (fun z => phi z * |z|) := by
  have h0 : MemLp id (1 : ENNReal) (gaussianReal 0 1) := by
    simpa using memLp_id_gaussianReal (μ := 0) (v := 1) 1
  have h : Integrable (fun x : ℝ => |x|) (gaussianReal 0 1) := by
    simpa [Real.norm_eq_abs] using (memLp_one_iff_integrable.mp h0).norm
  rw [gaussianReal_of_var_ne_zero 0 one_ne_zero] at h
  have h2 := (integrable_withDensity_iff_integrable_smul' (measurable_gaussianPDF 0 1)
    (ae_of_all _ fun _ => gaussianPDF_lt_top)).mp h
  simpa [toReal_gaussianPDF, phi] using h2

theorem integrable_phi_mul_three_add_abs : Integrable (fun z => phi z * (3 + |z|)) := by
  have := (integrable_phi.const_mul 3).add integrable_phi_mul_abs
  refine this.congr (ae_of_all _ fun z => ?_)
  simp only [Pi.add_apply]; ring

theorem continuous_aFun (ρ τ : ℝ) : Continuous (fun z => aFun ρ τ z) := by
  unfold aFun
  exact (continuous_const.sub (continuous_const.mul continuous_id)).div_const _

theorem integrable_phi_pMin {m : ℕ} (ρ : Fin m → ℝ) (τ : ℝ) :
    Integrable (fun z => phi z * pMin (fun i => aFun (ρ i) τ z)) := by
  have hc : Continuous fun z => pMin (fun i => aFun (ρ i) τ z) :=
    continuous_pMin.comp (continuous_pi fun i => continuous_aFun (ρ i) τ)
  refine integrable_phi.mono' (continuous_phi.mul hc).aestronglyMeasurable
    (ae_of_all _ fun z => ?_)
  rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg (phi_nonneg z), abs_of_nonneg (pMin_nonneg _)]
  exact mul_le_of_le_one_right (phi_nonneg z) (pMin_le_one _)

/-! ## The estimate -/

/-- Total Lipschitz constant of the floor vector `r`. -/
def lipSum {m : ℕ} (r : Fin m → ℝ) : ℝ := ∑ i, lipConst (Real.sqrt (1 - r i ^ 2))

theorem lipSum_nonneg {m : ℕ} {r : Fin m → ℝ} (hr : ∀ i, 0 < r i ∧ r i < 1) : 0 ≤ lipSum r :=
  Finset.sum_nonneg fun i _ => lipConst_nonneg (Real.sqrt_pos.mpr (by
    nlinarith [hr i]))

theorem pMin_diff_le {m : ℕ} {r r' : Fin m → ℝ} {η : ℝ} (hη0 : 0 < η) (hη : η ≤ 1 / 2)
    (hr : ∀ i, 0 < r i ∧ r i < 1) (hr' : ∀ i, (1 - η) * r i ≤ r' i ∧ r' i ≤ r i)
    {τ : ℝ} (hτ : |τ| ≤ 3) (z : ℝ) :
    |pMin (fun i => aFun (r i) τ z) - pMin (fun i => aFun (r' i) τ z)| ≤
      (3 + |z|) * (η * lipSum r / 2) := by
  refine (abs_pMin_sub_le _ _).trans ?_
  have hterm : ∀ i, |aFun (r i) τ z - aFun (r' i) τ z| / 2 ≤
      (3 + |z|) * (η * lipConst (Real.sqrt (1 - r i ^ 2)) / 2) := by
    intro i
    obtain ⟨h0, h1⟩ := hr i
    obtain ⟨h2, h3⟩ := hr' i
    have hpos : 0 < r' i := by nlinarith
    have hsq : 0 < Real.sqrt (1 - r i ^ 2) := Real.sqrt_pos.mpr (by nlinarith)
    have hle : Real.sqrt (1 - r i ^ 2) ≤ Real.sqrt (1 - r' i ^ 2) :=
      Real.sqrt_le_sqrt (by nlinarith)
    have hl := aFun_sub_le (ρ := r i) (ρ' := r' i) (s₀ := Real.sqrt (1 - r i ^ 2)) τ z
      (by rw [abs_of_pos h0]; exact h1.le) (by rw [abs_of_pos hpos]; linarith) hsq le_rfl hle
    have hD : |r i - r' i| ≤ η := by
      rw [abs_of_nonneg (by linarith)]; nlinarith
    have hL := lipConst_nonneg hsq
    have h4 : |τ| + |z| ≤ 3 + |z| := by linarith
    have h5 : (|τ| + |z|) * lipConst (Real.sqrt (1 - r i ^ 2)) * |r i - r' i| ≤
        (3 + |z|) * lipConst (Real.sqrt (1 - r i ^ 2)) * η := by
      gcongr
    nlinarith
  refine (Finset.sum_le_sum fun i _ => hterm i).trans (le_of_eq ?_)
  unfold lipSum
  simp only [Finset.mul_sum, Finset.sum_div]

theorem starBound_le_add {m : ℕ} {r r' : Fin m → ℝ} {η : ℝ} (hη0 : 0 < η) (hη : η ≤ 1 / 2)
    (hr : ∀ i, 0 < r i ∧ r i < 1) (hr' : ∀ i, (1 - η) * r i ≤ r' i ∧ r' i ≤ r i)
    {τ : ℝ} (hτ : |τ| ≤ 3) :
    starBound r' τ ≤ starBound r τ +
      (η * lipSum r / 2) * ∫ z, phi z * (3 + |z|) := by
  have hI := integrable_phi_pMin r τ
  have hI' := integrable_phi_pMin r' τ
  set c := η * lipSum r / 2 with hc
  unfold starBound
  have hsub : (∫ z in Set.Ioi τ, phi z * pMin (fun i => (τ - r i * z) / Real.sqrt (1 - r i ^ 2)))
      - (∫ z in Set.Ioi τ, phi z * pMin (fun i => (τ - r' i * z) / Real.sqrt (1 - r' i ^ 2)))
      ≤ c * ∫ z, phi z * (3 + |z|) := by
    change (∫ z in Set.Ioi τ, phi z * pMin (fun i => aFun (r i) τ z)) -
      (∫ z in Set.Ioi τ, phi z * pMin (fun i => aFun (r' i) τ z)) ≤ _
    rw [← integral_sub hI.integrableOn hI'.integrableOn]
    have hint : Integrable (fun z => phi z * ((3 + |z|) * c)) := by
      have := integrable_phi_mul_three_add_abs.mul_const c
      refine this.congr (ae_of_all _ fun z => ?_)
      simp only; ring
    calc ∫ z in Set.Ioi τ, (phi z * pMin (fun i => aFun (r i) τ z) -
          phi z * pMin (fun i => aFun (r' i) τ z))
        ≤ ∫ z in Set.Ioi τ, phi z * ((3 + |z|) * c) := by
          refine setIntegral_mono_on (hI.sub hI').integrableOn hint.integrableOn
            measurableSet_Ioi fun z _ => ?_
          have := pMin_diff_le hη0 hη hr hr' hτ z
          have h2 := (le_abs_self _).trans this
          have h3 : phi z * (pMin (fun i => aFun (r i) τ z) - pMin (fun i => aFun (r' i) τ z))
              ≤ phi z * ((3 + |z|) * c) := mul_le_mul_of_nonneg_left h2 (phi_nonneg z)
          linarith
      _ ≤ ∫ z, phi z * ((3 + |z|) * c) :=
          setIntegral_le_integral hint (ae_of_all _ fun z => by
            have : 0 ≤ c := by
              have := lipSum_nonneg hr
              positivity
            positivity [phi_nonneg z])
      _ = c * ∫ z, phi z * (3 + |z|) := by
          rw [← integral_const_mul]
          refine integral_congr_ae (ae_of_all _ fun z => ?_)
          simp only; ring
  linarith

/-- (B2) Continuity of the star bound from below in the floors. -/
theorem starBoundCont : StarBoundContClaim := by
  intro d r hr δ hδ
  set M := ∫ z, phi z * (3 + |z|) with hM
  have hM0 : 0 ≤ M := integral_nonneg fun z => mul_nonneg (phi_nonneg z) (by positivity)
  set B := lipSum r / 2 * M with hB
  have hB0 : 0 ≤ B := by
    have := lipSum_nonneg hr
    positivity
  refine ⟨min (1 / 2) (δ / (B + 1)), lt_min (by norm_num) (by positivity), ?_⟩
  intro r' hr' τ hτ
  set η := min (1 / 2) (δ / (B + 1)) with hη
  have hη0 : 0 < η := lt_min (by norm_num) (by positivity)
  have hη1 : η ≤ 1 / 2 := min_le_left _ _
  have hη2 : η ≤ δ / (B + 1) := min_le_right _ _
  have hτ' : |τ| ≤ 3 := abs_le.mpr ⟨hτ.1, hτ.2⟩
  have h := starBound_le_add hη0 hη1 hr hr' hτ'
  have hfin : η * lipSum r / 2 * M ≤ δ := by
    have e : η * lipSum r / 2 * M = η * B := by rw [hB]; ring
    rw [e]
    calc η * B ≤ δ / (B + 1) * B := mul_le_mul_of_nonneg_right hη2 hB0
      _ = δ * (B / (B + 1)) := by ring
      _ ≤ δ * 1 := by
          gcongr
          rw [div_le_one (by positivity)]; linarith
      _ = δ := mul_one δ
  linarith

end T2
end CubicPathwidth

#print axioms CubicPathwidth.T2.starBoundCont