CubicPathwidth.T2.HetStar

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

import CubicPathwidth.T2.DefsB
import CubicPathwidth.T2.StarFour
import CubicPathwidth.T2.Slepian
import CubicPathwidth.T2.Bridge

/-!
# The heterogeneous star bound (O4 with one floor per neighbor)

`hetStar : HetStarClaim`.

Variant of `starFour_of`: one floor `r i` per neighbor, no padding to four neighbors and no
simplex comparison.  The route is

1. lower each correlation `ρ_i = ⟪a, b_i⟫` to `r_i` by the coupling
   `c_i = b_i - (ρ_i - r_i) a + √(ρ_i² - r_i²) ξ_i` (fresh orthonormal `ξ_i`);
   Slepian compares `(a, c)` with `(a, b)`;
2. condition on `⟪a, x⟫ = z`: the leaves of `(a, c)` become `r_i z + s_i U_i` with unit
   `U_i ⟂ a`, and the conditional orthant probability is at least `pMin`;
3. integrate against the Gaussian density.
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory

namespace CubicPathwidth
namespace T2
namespace HetStar

open GaussianField (Sample)
open StarFour (allAbove pad xi inner_pad inner_pad_xi inner_xi_pad inner_xi_xi
  allAbove_eq_of_gram_eq inner_self_one norm_eq_one_of_inner_self prob_unit_gt)

/-! ## Orthants and `pMin` -/

/-- Strict upper orthant with thresholds `a`. -/
def orth {d : ℕ} (a : Fin d → ℝ) : Set (EuclideanSpace ℝ (Fin d)) := {y | ∀ i, a i < y i}

theorem measurableSet_orth {d : ℕ} (a : Fin d → ℝ) : MeasurableSet (orth a) := by
  have : orth a = ⋂ i, {y : EuclideanSpace ℝ (Fin d) | a i < y i} := by
    ext y; simp [orth]
  rw [this]
  exact MeasurableSet.iInter fun i =>
    measurableSet_lt measurable_const (by fun_prop)

theorem gaussProb_mono {d : ℕ} (S : Matrix (Fin d) (Fin d) ℝ)
    {A B : Set (EuclideanSpace ℝ (Fin d))} (h : A ⊆ B) : gaussProb S A ≤ gaussProb S B :=
  ENNReal.toReal_mono (measure_ne_top _ _) (measure_mono h)

theorem gaussProb_nonneg {d : ℕ} (S : Matrix (Fin d) (Fin d) ℝ)
    (A : Set (EuclideanSpace ℝ (Fin d))) : 0 ≤ gaussProb S A := ENNReal.toReal_nonneg

instance corrNonempty (d : ℕ) : Nonempty {C : Matrix (Fin d) (Fin d) ℝ // IsCorrelation C} :=
  ⟨⟨1, Matrix.PosSemidef.one, fun i => by simp⟩⟩

theorem pMin_bdd {d : ℕ} (a : Fin d → ℝ) :
    BddBelow (Set.range fun C : {C : Matrix (Fin d) (Fin d) ℝ // IsCorrelation C} =>
      gaussProb C.1 {x | ∀ i, a i < x i}) :=
  ⟨0, by rintro _ ⟨_, rfl⟩; exact gaussProb_nonneg _ _⟩

theorem pMin_nonneg {d : ℕ} (a : Fin d → ℝ) : 0 ≤ pMin a :=
  le_ciInf fun _ => gaussProb_nonneg _ _

theorem pMin_le {d : ℕ} (a : Fin d → ℝ) {C : Matrix (Fin d) (Fin d) ℝ} (hC : IsCorrelation C) :
    pMin a ≤ gaussProb C {x | ∀ i, a i < x i} :=
  ciInf_le (pMin_bdd a) (⟨C, hC⟩ : {C : Matrix (Fin d) (Fin d) ℝ // IsCorrelation C})

theorem pMin_anti {d : ℕ} {a a' : Fin d → ℝ} (h : ∀ i, a i ≤ a' i) : pMin a' ≤ pMin a :=
  ciInf_mono (pMin_bdd a') fun _ =>
    gaussProb_mono _ fun _ hx i => lt_of_le_of_lt (h i) (hx i)

/-- The conditional threshold. -/
def thr {d : ℕ} (r : Fin d → ℝ) (τ z : ℝ) : Fin d → ℝ :=
  fun i => (τ - r i * z) / Real.sqrt (1 - r i ^ 2)

theorem thr_anti {d : ℕ} {r : Fin d → ℝ} (hr : ∀ i, 0 < r i ∧ r i < 1) (τ : ℝ) {z z' : ℝ}
    (h : z ≤ z') : ∀ i, thr r τ z' i ≤ thr r τ z i := by
  intro i
  have hs : 0 < Real.sqrt (1 - r i ^ 2) :=
    Real.sqrt_pos.mpr (by nlinarith [(hr i).1, (hr i).2])
  unfold thr
  have : r i * z ≤ r i * z' := mul_le_mul_of_nonneg_left h (hr i).1.le
  exact div_le_div_of_nonneg_right (by linarith) hs.le

theorem monotone_pMin_thr {d : ℕ} {r : Fin d → ℝ} (hr : ∀ i, 0 < r i ∧ r i < 1) (τ : ℝ) :
    Monotone fun z => pMin (thr r τ z) :=
  fun _ _ h => pMin_anti (thr_anti hr τ h)

/-! ## A star family and its unit residuals -/

/-- A star family: unit center `w 0`, unit leaves, center-leaf correlations `r i`. -/
def IsHStar {M d : ℕ} (r : Fin d → ℝ) (w : Fin (d + 1) → Sample M) : Prop :=
  ‖w 0‖ = 1 ∧ (∀ i : Fin d, ‖w i.succ‖ = 1) ∧ ∀ i : Fin d, ⟪w 0, w i.succ⟫ = r i

/-- The unit residual of each leaf. -/
def Uh {M d : ℕ} (r : Fin d → ℝ) (w : Fin (d + 1) → Sample M) (i : Fin d) : Sample M :=
  (Real.sqrt (1 - r i ^ 2))⁻¹ • (w i.succ - r i • w 0)

section star

variable {M d : ℕ} {r : Fin d → ℝ} {w : Fin (d + 1) → Sample M}

theorem sqrt_pos'' (hr : ∀ i, 0 < r i ∧ r i < 1) (i : Fin d) : 0 < Real.sqrt (1 - r i ^ 2) :=
  Real.sqrt_pos.mpr (by nlinarith [(hr i).1, (hr i).2])

theorem sq_sqrt'' (hr : ∀ i, 0 < r i ∧ r i < 1) (i : Fin d) :
    Real.sqrt (1 - r i ^ 2) ^ 2 = 1 - r i ^ 2 :=
  Real.sq_sqrt (by nlinarith [(hr i).1, (hr i).2])

theorem inner_w0_Uh (hw : IsHStar r w) (i : Fin d) : ⟪w 0, Uh r w i⟫ = 0 := by
  obtain ⟨h0, -, hc⟩ := hw
  simp only [Uh, real_inner_smul_right, inner_sub_right, hc, inner_self_one h0]
  ring

theorem norm_Uh (hr : ∀ i, 0 < r i ∧ r i < 1) (hw : IsHStar r w) (i : Fin d) :
    ‖Uh r w i‖ = 1 := by
  obtain ⟨h0, h1, hc⟩ := hw
  have hs := sqrt_pos'' hr i
  have h2 := sq_sqrt'' hr i
  have e : ⟪Uh r w i, Uh r w i⟫ = 1 := by
    simp only [Uh, real_inner_smul_left, real_inner_smul_right, inner_sub_left, inner_sub_right,
      inner_self_one h0, inner_self_one (h1 i), real_inner_comm (w 0) (w i.succ), hc]
    generalize Real.sqrt (1 - r i ^ 2) = s at hs h2 ⊢
    have hp : 1 - r i ^ 2 = s ^ 2 := h2.symm
    field_simp
    nlinarith [hp]
  exact norm_eq_one_of_inner_self e

theorem inner_succ_eq' (hr : ∀ i, 0 < r i ∧ r i < 1) (i : Fin d) (x : Sample M) :
    ⟪w i.succ, x⟫ = r i * ⟪w 0, x⟫ + Real.sqrt (1 - r i ^ 2) * ⟪Uh r w i, x⟫ := by
  have hs := sqrt_pos'' hr i
  simp only [Uh, real_inner_smul_left, inner_sub_left]
  field_simp
  ring

end star

/-! ## Conditioning on the center -/

/-- The conditional orthant probability at center value `z`. -/
def Fz {d : ℕ} (C : Matrix (Fin d) (Fin d) ℝ) (r : Fin d → ℝ) (τ z : ℝ) : ℝ :=
  if τ < z then gaussProb C (orth (thr r τ z)) else 0

theorem allAbove_het {M d : ℕ} {r : Fin d → ℝ} (hr : ∀ i, 0 < r i ∧ r i < 1)
    {w : Fin (d + 1) → Sample M} (hw : IsHStar r w) (τ : ℝ) :
    allAbove w τ = ∫ z, Fz (gram (Uh r w)) r τ z ∂gaussianReal 0 1 ∧
      Integrable (fun z => Fz (gram (Uh r w)) r τ z) (gaussianReal 0 1) := by
  have hworth := inner_w0_Uh hw
  set a := w 0 with ha_def
  have ha : ‖a‖ = 1 := hw.1
  set U := Uh r w with hU
  set S : Set (ℝ × Sample M) :=
    {p | τ < p.1 ∧ ∀ i : Fin d,
      τ < r i * p.1 + Real.sqrt (1 - r i ^ 2) * ⟪U i, p.2⟫} with hS_def
  have hS : MeasurableSet S := by
    have : S = {p : ℝ × Sample M | τ < p.1} ∩
        ⋂ i : Fin d, {p : ℝ × Sample M |
          τ < r i * p.1 + Real.sqrt (1 - r i ^ 2) * ⟪U i, p.2⟫} := by
      ext p; simp [S]
    rw [this]
    exact (measurableSet_lt measurable_const measurable_fst).inter
      (MeasurableSet.iInter fun i => measurableSet_lt measurable_const (by fun_prop))
  have hev : {x : Sample M | ∀ j, τ < ⟪w j, x⟫} =
      {x | (⟪a, x⟫, C3.remainder a x) ∈ S} := by
    ext x
    simp only [Set.mem_ofPred_eq, S, C3.inner_remainder_of_orth (hworth _)]
    rw [Fin.forall_fin_succ]
    simp only [inner_succ_eq' (w := w) hr, ha_def, hU]
  have hint : ∀ z, (stdGaussian (Sample M)).real {x | (z, C3.remainder a x) ∈ S} =
      Fz (gram U) r τ z := by
    intro z
    unfold Fz
    by_cases hz : τ < z
    · simp only [hz, ↓reduceIte]
      rw [bridge M d U _ (measurableSet_orth _)]
      congr 1
      ext x
      simp only [S, Set.mem_ofPred_eq, orth, thr, hz, true_and,
        C3.inner_remainder_of_orth (hworth _)]
      change _ ↔ ∀ i, _ < ⟪U i, x⟫
      refine forall_congr' fun i => ?_
      have hs := sqrt_pos'' hr i
      rw [div_lt_iff₀ hs]
      constructor <;> intro h <;> linarith
    · simp only [hz, ↓reduceIte]
      have : {x : Sample M | (z, C3.remainder a x) ∈ S} = ∅ := by
        ext x; simp [S, hz]
      rw [this, measureReal_empty]
  have hfun : (fun z => Fz (gram U) r τ z) =
      fun z => (stdGaussian (Sample M)).real {x | (z, C3.remainder a x) ∈ S} := by
    funext z; exact (hint z).symm
  refine ⟨?_, ?_⟩
  · unfold allAbove
    rw [hev, C3.real_disintegrate ha hS]
    exact integral_congr_ae (ae_of_all _ fun z => hint z)
  · rw [hfun]
    exact C3.integrable_cond hS

/-- The integral lower bound for the all-above probability of a star family. -/
theorem allAbove_het_ge {M d : ℕ} {r : Fin d → ℝ} (hr : ∀ i, 0 < r i ∧ r i < 1)
    {w : Fin (d + 1) → Sample M} (hw : IsHStar r w) (τ : ℝ) :
    (∫ z in Set.Ioi τ, phi z * pMin (thr r τ z)) ≤ allAbove w τ := by
  obtain ⟨e, hI⟩ := allAbove_het hr hw τ
  rw [e]
  set g : ℝ → ℝ := (Set.Ioi τ).indicator (fun z => pMin (thr r τ z)) with hg
  have hgm : Measurable g :=
    (monotone_pMin_thr hr τ).measurable.indicator measurableSet_Ioi
  have hgle : ∀ z, g z ≤ Fz (gram (Uh r w)) r τ z := by
    intro z
    unfold Fz
    by_cases hz : τ < z
    · simp only [hg, Set.indicator_of_mem (Set.mem_Ioi.mpr hz), hz, ↓reduceIte]
      refine pMin_le _ ⟨gram_posSemidef _, fun i => ?_⟩
      show ⟪Uh r w i, Uh r w i⟫ = 1
      exact inner_self_one (norm_Uh hr hw i)
    · simp only [hg, Set.indicator_of_notMem (show z ∉ Set.Ioi τ from hz), hz, ↓reduceIte]
      exact le_rfl
  have hg0 : ∀ z, 0 ≤ g z := by
    intro z
    by_cases hz : τ < z
    · simp only [hg, Set.indicator_of_mem (Set.mem_Ioi.mpr hz)]
      exact pMin_nonneg _
    · simp only [hg, Set.indicator_of_notMem (show z ∉ Set.Ioi τ from hz)]
      exact le_rfl
  have hgi : Integrable g (gaussianReal 0 1) :=
    Integrable.mono' hI hgm.aestronglyMeasurable
      (ae_of_all _ fun z => by
        rw [Real.norm_eq_abs, abs_of_nonneg (hg0 z)]; exact hgle z)
  have h1 : (∫ z in Set.Ioi τ, phi z * pMin (thr r τ z)) = ∫ z, g z ∂gaussianReal 0 1 := by
    rw [integral_gaussianReal_eq_integral_smul (by norm_num : (1 : NNReal) ≠ 0)]
    rw [← integral_indicator measurableSet_Ioi]
    refine integral_congr_ae (ae_of_all _ fun z => ?_)
    by_cases hz : z ∈ Set.Ioi τ
    · simp [hg, hz, phi]
    · simp [hg, hz]
  rw [h1]
  exact integral_mono hgi hI hgle

/-! ## Lowering the incident correlations to `r` -/

/-- The comparison star: center `A`, leaves `B_i - (ρ_i - r_i) A + √(ρ_i² - r_i²) ξ_i`. -/
def hcfam {N d : ℕ} (r : Fin d → ℝ) (A : Sample N) (B ξ : Fin d → Sample N) (ρ : Fin d → ℝ) :
    Fin (d + 1) → Sample N :=
  Fin.cons A (fun i => B i - (ρ i - r i) • A + Real.sqrt (ρ i ^ 2 - r i ^ 2) • ξ i)

section hcfam

variable {N d : ℕ} {r : Fin d → ℝ} {A : Sample N} {B ξ : Fin d → Sample N} {ρ : Fin d → ℝ}

theorem inner_hcfam_succ (hA : ⟪A, A⟫ = 1) (hAB : ∀ i, ⟪A, B i⟫ = ρ i)
    (hAξ : ∀ i, ⟪A, ξ i⟫ = 0) (hBξ : ∀ i j, ⟪B i, ξ j⟫ = 0)
    (hξ : ∀ i j, ⟪ξ i, ξ j⟫ = if i = j then 1 else 0) (i j : Fin d) :
    ⟪hcfam r A B ξ ρ i.succ, hcfam r A B ξ ρ j.succ⟫ =
      ⟪B i, B j⟫ - ρ i * ρ j + r i * r j +
        (if i = j then Real.sqrt (ρ i ^ 2 - r i ^ 2) * Real.sqrt (ρ j ^ 2 - r j ^ 2) else 0) := by
  have e1 : ⟪B i, A⟫ = ρ i := by rw [real_inner_comm, hAB]
  have e2 : ⟪ξ i, A⟫ = 0 := by rw [real_inner_comm, hAξ]
  have e3 : ⟪ξ i, B j⟫ = 0 := by rw [real_inner_comm, hBξ]
  simp only [hcfam, Fin.cons_succ, inner_add_left, inner_add_right, inner_sub_left,
    inner_sub_right, real_inner_smul_left, real_inner_smul_right, hA, hAB, hAξ, hBξ, hξ, e1, e2,
    e3]
  by_cases h : i = j
  · subst h; simp; ring
  · simp [h]; ring

theorem inner_hcfam_zero_succ (hA : ⟪A, A⟫ = 1) (hAB : ∀ i, ⟪A, B i⟫ = ρ i)
    (hAξ : ∀ i, ⟪A, ξ i⟫ = 0) (i : Fin d) :
    ⟪hcfam r A B ξ ρ 0, hcfam r A B ξ ρ i.succ⟫ = r i := by
  simp only [hcfam, Fin.cons_zero, Fin.cons_succ, inner_add_right, inner_sub_right,
    real_inner_smul_right, hA, hAB, hAξ]
  ring

theorem isHStar_hcfam (hA : ⟪A, A⟫ = 1) (hAB : ∀ i, ⟪A, B i⟫ = ρ i)
    (hAξ : ∀ i, ⟪A, ξ i⟫ = 0) (hBξ : ∀ i j, ⟪B i, ξ j⟫ = 0)
    (hξ : ∀ i j, ⟪ξ i, ξ j⟫ = if i = j then 1 else 0) (hBn : ∀ i, ⟪B i, B i⟫ = 1)
    (hρ : ∀ i, r i ≤ ρ i) (hr : ∀ i, 0 < r i) : IsHStar r (hcfam r A B ξ ρ) := by
  refine ⟨?_, fun i => ?_, fun i => ?_⟩
  · apply norm_eq_one_of_inner_self
    simpa [hcfam] using hA
  · apply norm_eq_one_of_inner_self
    rw [inner_hcfam_succ hA hAB hAξ hBξ hξ, hBn]
    simp only [↓reduceIte]
    have : 0 ≤ ρ i ^ 2 - r i ^ 2 := by nlinarith [hρ i, hr i]
    rw [Real.mul_self_sqrt this]
    ring
  · exact inner_hcfam_zero_succ hA hAB hAξ i

end hcfam

/-! ## Frontier versus all-above -/

theorem frontier_eq {M d : ℕ} (a : Sample M) (b : Fin d → Sample M) (τ : ℝ) :
    (stdGaussian (Sample M)).real {x | τ < ⟪a, x⟫ ∧ ∃ i, ⟪b i, x⟫ ≤ τ} =
      (stdGaussian (Sample M)).real {x | τ < ⟪a, x⟫} -
        allAbove (Fin.cons a b : Fin (d + 1) → Sample M) τ := by
  unfold allAbove
  have hB : MeasurableSet {x : Sample M | ∀ j, τ < ⟪(Fin.cons a b : Fin (d + 1) → Sample M) j, x⟫} := by
    have : {x : Sample M | ∀ j, τ < ⟪(Fin.cons a b : Fin (d + 1) → Sample M) j, x⟫} =
        ⋂ j, {x | τ < ⟪(Fin.cons a b : Fin (d + 1) → Sample M) j, x⟫} := by
      ext x; simp
    rw [this]
    exact MeasurableSet.iInter fun j => measurableSet_lt measurable_const (by fun_prop)
  have hsub : {x : Sample M | ∀ j, τ < ⟪(Fin.cons a b : Fin (d + 1) → Sample M) j, x⟫} ⊆
      {x | τ < ⟪a, x⟫} := fun x hx => by simpa using hx 0
  rw [← measureReal_sdiff hsub hB]
  congr 1
  ext x
  simp only [Set.mem_ofPred_eq, Set.mem_sdiff, not_forall, not_lt]
  constructor
  · rintro ⟨h0, i, hi⟩
    exact ⟨h0, i.succ, by simpa using hi⟩
  · rintro ⟨h0, j, hj⟩
    refine ⟨h0, ?_⟩
    induction j using Fin.cases with
    | zero => exact absurd h0 (not_lt.mpr (by simpa using hj))
    | succ i => exact ⟨i, by simpa using hj⟩

theorem Phi_neg_eq (τ : ℝ) : Phi (-τ) = (gaussianReal 0 1).real (Set.Ioi τ) := by
  unfold Phi
  have : NullSingletonClass (gaussianReal 0 1) :=
    nullSingletonClass_gaussianReal (by norm_num)
  have h := gaussianReal_map_neg (μ := 0) (v := 1)
  rw [neg_zero] at h
  have e : Set.Iic (-τ) = (fun x : ℝ => -x) ⁻¹' (Set.Ici τ) := by
    ext x; simp
  rw [e, ← map_measureReal_apply measurable_neg measurableSet_Ici, h]
  exact measureReal_congr Ioi_ae_eq_Ici.symm

/-! ## The main theorem -/

theorem main : HetStarClaim := by
  intro m d r hr a b ha hbn hab τ
  have hr0 : ∀ i, 0 < r i := fun i => (hr i).1
  set A : Sample (m + d) := pad d a with hA_def
  set B : Fin d → Sample (m + d) := fun i => pad d (b i) with hB_def
  set ρ : Fin d → ℝ := fun i => ⟪a, b i⟫ with hρ_def
  set ξ : Fin d → Sample (m + d) := xi m d with hξ_def
  have haa : ⟪A, A⟫ = 1 := by rw [hA_def, inner_pad]; exact inner_self_one ha
  have hA1 : ‖A‖ = 1 := norm_eq_one_of_inner_self haa
  have hAB : ∀ i, ⟪A, B i⟫ = ρ i := fun i => inner_pad d a (b i)
  have hAξ : ∀ i, ⟪A, ξ i⟫ = 0 := fun i => inner_pad_xi d a i
  have hBξ : ∀ i j, ⟪B i, ξ j⟫ = 0 := fun i j => inner_pad_xi d (b i) j
  have hξξ : ∀ i j, ⟪ξ i, ξ j⟫ = if i = j then 1 else 0 := fun i j => inner_xi_xi m d i j
  have hBn : ∀ i, ⟪B i, B i⟫ = 1 := fun i => by
    rw [hB_def]; simp only; rw [inner_pad]; exact inner_self_one (hbn i)
  have hstar : IsHStar r (hcfam r A B ξ ρ) :=
    isHStar_hcfam haa hAB hAξ hBξ hξξ hBn hab hr0
  -- lower bound for the comparison star
  have step1 := allAbove_het_ge hr hstar τ
  -- Slepian
  have step2 : allAbove (hcfam r A B ξ ρ) τ ≤
      allAbove (Fin.cons A B : Fin (d + 1) → Sample (m + d)) τ := by
    have hn1 : ∀ i, ‖hcfam r A B ξ ρ i‖ = 1 := by
      intro i
      induction i using Fin.cases with
      | zero => exact hstar.1
      | succ i => exact hstar.2.1 i
    have hn2 : ∀ i, ‖(Fin.cons A B : Fin (d + 1) → Sample (m + d)) i‖ = 1 := by
      intro i
      induction i using Fin.cases with
      | zero => simpa using hA1
      | succ i => simpa using norm_eq_one_of_inner_self (hBn i)
    have hle : ∀ i j, i ≠ j → ⟪hcfam r A B ξ ρ i, hcfam r A B ξ ρ j⟫ ≤
        ⟪(Fin.cons A B : Fin (d + 1) → Sample (m + d)) i,
          (Fin.cons A B : Fin (d + 1) → Sample (m + d)) j⟫ := by
      intro i j hij
      induction i using Fin.cases with
      | zero =>
        induction j using Fin.cases with
        | zero => exact absurd rfl hij
        | succ j =>
          rw [inner_hcfam_zero_succ haa hAB hAξ]
          simpa [hAB] using hab j
      | succ i =>
        induction j using Fin.cases with
        | zero =>
          rw [real_inner_comm, inner_hcfam_zero_succ haa hAB hAξ, real_inner_comm]
          simpa [hAB] using hab i
        | succ j =>
          have hij' : i ≠ j := fun h => hij (h ▸ rfl)
          rw [inner_hcfam_succ haa hAB hAξ hBξ hξξ]
          simp only [hij', ↓reduceIte, add_zero, Fin.cons_succ]
          have : r i * r j ≤ ρ i * ρ j := by
            have := hab i
            have := hab j
            have := hr0 i
            have := hr0 j
            nlinarith
          linarith
    exact slepian (m + d) (d + 1) (hcfam r A B ξ ρ) (Fin.cons A B)
      (fun i => by rw [hn1, hn2]) hle (fun _ => τ)
  -- transfer back to `Sample m`
  have step3 : allAbove (Fin.cons A B : Fin (d + 1) → Sample (m + d)) τ =
      allAbove (Fin.cons a b : Fin (d + 1) → Sample m) τ := by
    have hfam : (Fin.cons A B : Fin (d + 1) → Sample (m + d)) =
        fun i => pad d ((Fin.cons a b : Fin (d + 1) → Sample m) i) := by
      funext i
      induction i using Fin.cases with
      | zero => simp [hA_def]
      | succ i => simp [hB_def]
    rw [hfam]
    exact allAbove_eq_of_gram_eq bridge _ _ (StarFour.gram_pad d _) τ
  have hsb : starBound r τ =
      Phi (-τ) - ∫ z in Set.Ioi τ, phi z * pMin (thr r τ z) := rfl
  rw [frontier_eq, prob_unit_gt ha, hsb, Phi_neg_eq]
  linarith

end HetStar

/-- **The heterogeneous star bound**: the frontier probability of a star with one correlation
floor per neighbor is at most `starBound r τ`. -/
theorem hetStar : HetStarClaim := HetStar.main

end T2
end CubicPathwidth

#print axioms CubicPathwidth.T2.hetStar