CubicPathwidth.Sw4.FrontierVertex

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

import CubicPathwidth.Sw4.Defs
import CubicPathwidth.Sw4.FrontierVertexNum
import CubicPathwidth.T2.HetStar
import CubicPathwidth.T2.StarBoundCont
import CubicPathwidth.C3.StarFrontier
import CubicPathwidth.C3.Constants
import CubicPathwidth.C3.GaussianTools
import CubicPathwidth.T3.Constants
import CubicPathwidth.T3.GoodLabelsCount5B

/-!
# Q4: the frontier vertex bound (manuscript Lemma A.14 (`lem:switch4-means`), per vertex)

`frontierVertex_of : SwitchedChargingClaim → FrontierVertexClaim`.

Route. The frontier probability at `τ ≠ 0` is at most the closed probability
`P(|τ|) = Pr(|τ| ≤ ⟨a,x⟩, ∃ i, ⟨b_i,x⟩ ≤ |τ|)` (for `τ < 0` use `x ↦ -x`).
* `|τ| ≤ 35/32`, type other than `(3; 3, 0)`: the closed and open events differ by a null
  event, `hetStar` bounds the open one by `starBound` at the lowered floors, and
  `starBoundCont` moves back to the type floors at cost `δ`; H7 closes the argument.
* `|τ| ≤ 35/32`, type `(3; 3, 0)`: `starFrontier` gives `κ((1-η) r*) ≤ c₃ + δ`, and the
  transfer term vanishes.
* `|τ| > 35/32`: the transfer is `0` and `P(|τ|) ≤ Φ(-35/32) < c₃ ≤ a_d`.
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory

namespace CubicPathwidth
namespace Sw4
namespace FV

open T2 T3

variable {m d : ℕ}

/-- The closed frontier probability `Pr(t ≤ ⟨a,x⟩, ∃ i, ⟨b_i,x⟩ ≤ t)`. -/
def closedProb (t : ℝ) (a : GaussianField.Sample m) (b : Fin d → GaussianField.Sample m) : ℝ :=
  (μ m).real {x | t ≤ ⟪a, x⟫ ∧ ∃ i, ⟪b i, x⟫ ≤ t}

theorem measurableSet_exists (p : Fin d → GaussianField.Sample m → Prop)
    (h : ∀ i, MeasurableSet {x | p i x}) : MeasurableSet {x | ∃ i, p i x} := by
  have : {x | ∃ i, p i x} = ⋃ i, {x | p i x} := by ext x; simp
  rw [this]
  exact MeasurableSet.iUnion h

theorem frontierProb_le_closed (τ : ℝ) (hτ : τ ≠ 0) (a : GaussianField.Sample m)
    (b : Fin d → GaussianField.Sample m) : frontierProb τ a b ≤ closedProb |τ| a b := by
  unfold frontierProb closedProb
  rcases lt_or_gt_of_ne hτ with hneg | hpos
  · have hnp : ¬ 0 < τ := not_lt.mpr hneg.le
    simp only [hnp, ↓reduceIte]
    rw [abs_of_neg hneg]
    have hmeas : MeasurableSet {x : GaussianField.Sample m | ⟪a, x⟫ ≤ τ ∧ ∃ i, τ < ⟪b i, x⟫} := by
      refine MeasurableSet.inter
        (measurableSet_le (show Measurable fun x : GaussianField.Sample m => ⟪a, x⟫ by fun_prop)
          measurable_const) ?_
      exact measurableSet_exists _ fun i => measurableSet_lt measurable_const
        (show Measurable fun x : GaussianField.Sample m => ⟪b i, x⟫ by fun_prop)
    rw [← C3.real_neg_preimage hmeas]
    refine measureReal_mono ?_
    rintro x ⟨h1, i, h2⟩
    refine ⟨?_, i, ?_⟩
    · rw [inner_neg_right] at h1; linarith
    · rw [inner_neg_right] at h2; linarith
  · simp only [hpos, ↓reduceIte]
    rw [abs_of_pos hpos]
    exact measureReal_mono fun x ⟨h1, h2⟩ => ⟨h1.le, h2⟩

theorem real_singleton_gaussian (t : ℝ) : (gaussianReal 0 1).real {t} = 0 := by
  have : NullSingletonClass (gaussianReal 0 1) := nullSingletonClass_gaussianReal (by norm_num)
  simp [Measure.real]

/-- The closed event exceeds the open event by a null event. -/
theorem closed_le_open {a : GaussianField.Sample m} (ha : ‖a‖ = 1)
    (b : Fin d → GaussianField.Sample m) (t : ℝ) :
    closedProb t a b ≤ (μ m).real {x | t < ⟪a, x⟫ ∧ ∃ i, ⟪b i, x⟫ ≤ t} := by
  unfold closedProb
  have hsub : {x : GaussianField.Sample m | t ≤ ⟪a, x⟫ ∧ ∃ i, ⟪b i, x⟫ ≤ t} ⊆
      {x | t < ⟪a, x⟫ ∧ ∃ i, ⟪b i, x⟫ ≤ t} ∪ {x | ⟪a, x⟫ ∈ ({t} : Set ℝ)} := by
    rintro x ⟨h1, h2⟩
    rcases h1.lt_or_eq with h | h
    · exact Or.inl ⟨h, h2⟩
    · exact Or.inr (by simp [h])
  refine (measureReal_mono hsub).trans ((measureReal_union_le _ _).trans ?_)
  rw [C3.real_unit_projection ha (measurableSet_singleton t), real_singleton_gaussian, add_zero]

/-- Large thresholds: the closed event is inside `{t ≤ ⟨a,x⟩}`. -/
theorem closed_le_Phi {a : GaussianField.Sample m} (ha : ‖a‖ = 1)
    (b : Fin d → GaussianField.Sample m) (t : ℝ) : closedProb t a b ≤ Phi (-t) := by
  unfold closedProb
  have hsub : {x : GaussianField.Sample m | t ≤ ⟪a, x⟫ ∧ ∃ i, ⟪b i, x⟫ ≤ t} ⊆
      {x | ⟪a, x⟫ ∈ Set.Ici t} := fun x hx => hx.1
  refine (measureReal_mono hsub).trans ?_
  rw [C3.real_unit_projection ha measurableSet_Ici, T2.GLC.Phi_neg_eq_Ici]

theorem Phi_mono {x y : ℝ} (h : x ≤ y) : Phi x ≤ Phi y := by
  unfold Phi
  exact measureReal_mono (Set.Iic_subset_Iic.mpr h)

/-- Choice of `η` for the pure cubic type. -/
theorem kappa_close {δ : ℝ} (hδ : 0 < δ) :
    ∃ η₂ : ℝ, 0 < η₂ ∧ ∀ η : ℝ, 0 < η → η ≤ η₂ →
      C3.kappa ((1 - η) * C3.rStar) ≤ C3.c3 + δ := by
  have hk : Continuous C3.kappa := by
    unfold C3.kappa C3.pairCorr
    fun_prop
  have hg : Continuous fun η : ℝ => C3.kappa ((1 - η) * C3.rStar) :=
    hk.comp (by fun_prop)
  obtain ⟨ε, hε, h⟩ := Metric.continuousAt_iff.1 (hg.continuousAt (x := 0)) δ hδ
  refine ⟨ε / 2, by positivity, fun η hη hηε => ?_⟩
  have h1 := h (x := η) (by rw [Real.dist_eq, sub_zero, abs_of_pos hη]; linarith)
  rw [Real.dist_eq] at h1
  have h0 : C3.kappa ((1 - 0) * C3.rStar) = C3.c3 := by simp [C3.kappa_rStar]
  rw [h0] at h1
  linarith [(abs_lt.mp h1).2]

theorem rStar_pos : 0 < C3.rStar := by
  unfold C3.rStar
  positivity

theorem typeFloors_three_three (i : Fin 3) : typeFloors 3 3 0 i = C3.rStar := by
  have hi : (i : ℕ) < 3 := i.2
  unfold typeFloors
  simp only [hi, ↓reduceIte]
  exact T3.rFloor_33

theorem transfer_zero (d k₃ k₄ : ℕ) : transferTerm d k₃ k₄ 0 0 0 0 = 0 := by
  unfold transferTerm
  split_ifs <;> simp

theorem coeff_ge_c3 (d : ℕ) (hd : d = 3 ∨ d = 4) : C3.c3 ≤ coeff C3.c3 aM 0 d := by
  unfold coeff
  rcases hd with rfl | rfl
  · simp
  · simpa using c3_le_aM

end FV

open T2 T3

/-- (Q4, Lemma A.14 (`lem:switch4-means`) per vertex) -/
theorem frontierVertex_of (h7 : SwitchedChargingClaim) : FrontierVertexClaim := by
  intro δ hδ
  obtain ⟨η₁, hη₁0, hη₁1, hη⟩ := T3.GLC5.eta_exists5 T2.starBoundCont hδ
  obtain ⟨η₂, hη₂0, hκ⟩ := FV.kappa_close hδ
  set η := min η₁ η₂ with hηdef
  have hη0 : 0 < η := lt_min hη₁0 hη₂0
  have hηle1 : η ≤ η₁ := min_le_left _ _
  have hηle2 : η ≤ η₂ := min_le_right _ _
  have hη1 : η < 1 := lt_of_le_of_lt hηle1 hη₁1
  refine ⟨η, hη0, fun τ hτ => ?_⟩
  set τ' := |τ| with hτ'
  have hτ'0 : 0 < τ' := abs_pos.mpr hτ
  by_cases hsmall : τ' ≤ 35 / 32
  · obtain ⟨t, ht⟩ := h7 τ' ⟨hτ'0.le, hsmall⟩
    refine ⟨t, fun m d k₃ k₄ a b hd hk ha hb hab => ?_⟩
    have hfc := FV.frontierProb_le_closed τ hτ a b
    rw [← hτ'] at hfc
    by_cases hT0 : d = 3 ∧ k₃ = 3
    · obtain ⟨rfl, rfl⟩ := hT0
      have hk4 : k₄ = 0 := by omega
      subst hk4
      have hrpos : 0 < (1 - η) * C3.rStar := by
        have := FV.rStar_pos; nlinarith
      have hrle : (1 - η) * C3.rStar ≤ C3.rStar := by
        have := FV.rStar_pos; nlinarith
      have hsf := C3.starFrontier m ((1 - η) * C3.rStar) hrpos hrle a 3 le_rfl b ha hb
        (fun i => by rw [← FV.typeFloors_three_three i]; exact hab i) τ' hτ'0.le
      have hκ' := hκ η hη0 hηle2
      have hco : coeff C3.c3 aM 0 3 = C3.c3 := by simp [coeff]
      have htr : transferTerm 3 3 0 0 t 0 0 = 0 := by simp [transferTerm]
      rw [htr, hco]
      unfold FV.closedProb at hfc
      linarith
    · -- other types: hetStar and continuity
      have hd' : d = 3 ∨ d = 4 ∨ d = 5 := by omega
      have hd3 : 3 ≤ d := by omega
      set r' : Fin d → ℝ := fun i => (1 - η) * typeFloors d k₃ k₄ i with hr'
      have hr'pos : ∀ i, 0 < r' i := fun i =>
        mul_pos (by linarith) (T3.GLC5.typeFloors_pos d k₃ k₄ i)
      have hr'lt : ∀ i, r' i < 1 := fun i => by
        have h1 := T3.GLC5.typeFloors_lt_one hd3 k₃ k₄ i
        have h2 := T3.GLC5.typeFloors_pos d k₃ k₄ i
        simp only [hr']
        nlinarith
      have hhet := T2.hetStar m d r' (fun i => ⟨hr'pos i, hr'lt i⟩) a b ha hb hab τ'
      have hopen := FV.closed_le_open ha b τ'
      have hcont := hη d k₃ k₄ hd' (by omega) (by omega) r'
        (fun i => by
          have h2 := T3.GLC5.typeFloors_pos d k₃ k₄ i
          refine ⟨?_, ?_⟩
          · simp only [hr']; nlinarith
          · simp only [hr']; nlinarith)
        τ' ⟨by linarith, by linarith⟩
      have hH := ht d k₃ k₄ hd hk hT0
      unfold FV.closedProb at hopen hfc
      have : frontierProb τ a b ≤ starBound r' τ' := by
        refine hfc.trans (hopen.trans ?_)
        exact hhet
      linarith
  · refine ⟨0, fun m d k₃ k₄ a b hd hk ha hb hab => ?_⟩
    have hfc := FV.frontierProb_le_closed τ hτ a b
    rw [← hτ'] at hfc
    have h1 := FV.closed_le_Phi (b := b) ha τ'
    have h2 : Phi (-τ') ≤ Phi (-(35 / 32)) := FV.Phi_mono (by linarith [not_le.mp hsmall])
    have h3 := FV.Phi_neg_lt_c3
    have h4 := FV.coeff_ge_c3 d hd
    rw [FV.transfer_zero]
    linarith

end Sw4
end CubicPathwidth

#print axioms CubicPathwidth.Sw4.frontierVertex_of