CubicPathwidth.T2.Bridge

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

import CubicPathwidth.T2.Defs
import Mathlib.Analysis.InnerProductSpace.GramMatrix

/-!
# The Gaussian bridge

`N(0, Gram w)` is the law of `(⟨w_j, x⟩)_j` for a standard Gaussian `x`
(`bridge : BridgeClaim`). Explicit vectors realizing the ideal-star covariance
and the regular-simplex Gram matrix in dimension four.
-/

noncomputable section
open scoped RealInnerProductSpace
open MeasureTheory ProbabilityTheory

namespace CubicPathwidth
namespace T2

open GaussianField (Sample)

theorem gram_eq_matrix_gram {m k : ℕ} (w : Fin k → Sample m) :
    gram w = Matrix.gram ℝ w := rfl

theorem gram_posSemidef {m k : ℕ} (w : Fin k → Sample m) : (gram w).PosSemidef :=
  Matrix.posSemidef_gram ℝ w

/-- The map `x ↦ (⟨w_j, x⟩)_j`. -/
def innerVec {m k : ℕ} (w : Fin k → Sample m) (x : Sample m) : EuclideanSpace ℝ (Fin k) :=
  WithLp.toLp 2 fun j => ⟪w j, x⟫

theorem continuous_innerVec {m k : ℕ} (w : Fin k → Sample m) : Continuous (innerVec w) :=
  (PiLp.continuous_toLp 2 _).comp (continuous_pi fun _ => continuous_const.inner continuous_id)

theorem measurable_innerVec {m k : ℕ} (w : Fin k → Sample m) : Measurable (innerVec w) :=
  (continuous_innerVec w).measurable

theorem inner_innerVec {m k : ℕ} (w : Fin k → Sample m) (x : Sample m)
    (t : EuclideanSpace ℝ (Fin k)) :
    ⟪innerVec w x, t⟫ = ⟪x, ∑ j, t j • w j⟫ := by
  simp only [innerVec, PiLp.inner_apply, inner_sum, real_inner_comm x]
  refine Finset.sum_congr rfl fun j _ => ?_
  simp only [RCLike.inner_apply, conj_trivial]
  rw [Finset.mul_sum]
  exact Finset.sum_congr rfl fun i _ => by simp only [PiLp.smul_apply, smul_eq_mul]; ring

theorem map_innerVec_eq {m k : ℕ} (w : Fin k → Sample m) :
    (stdGaussian (Sample m)).map (innerVec w) = multivariateGaussian 0 (gram w) := by
  apply Measure.ext_of_charFun
  ext t
  rw [charFun_multivariateGaussian (gram_posSemidef w), charFun_apply,
    integral_map (measurable_innerVec w).aemeasurable (by fun_prop)]
  simp_rw [inner_innerVec]
  rw [← charFun_apply, charFun_stdGaussian]
  have hq : t.ofLp ⬝ᵥ (gram w).mulVec t.ofLp = ‖∑ j, t j • w j‖ ^ 2 := by
    have := Matrix.star_dotProduct_gram_mulVec (𝕜 := ℝ) w t.ofLp t.ofLp
    rw [star_trivial] at this
    rw [gram_eq_matrix_gram, this, real_inner_self_eq_norm_sq]
  rw [hq]
  simp [neg_div]

theorem bridge : BridgeClaim := by
  intro m k w A hA
  have h := map_innerVec_eq w
  rw [gaussProb, ← h, Measure.map_apply (measurable_innerVec w) hA, measureReal_def]
  rfl

/-! ## Explicit vectors -/

/-- Coordinates of the ideal 4-star vectors: the center is `e₀`, and leaf `i`
is `r e₀ + √(1-r²) u_i` with `u_i ∈ {(1,1,1),(1,-1,-1),(-1,1,-1),(-1,-1,1)}/√3`
in coordinates `1,2,3`. Here `√((1-r²)/3) = √(1-r²)/√3`. -/
def starCoord (r : ℝ) : Fin 5 → Fin 4 → ℝ :=
  let q := Real.sqrt ((1 - r ^ 2) / 3)
  ![![1, 0, 0, 0], ![r, q, q, q], ![r, q, -q, -q], ![r, -q, q, -q], ![r, -q, -q, q]]

/-- The ideal 4-star vectors. -/
def starVec (r : ℝ) (i : Fin 5) : Sample 4 := WithLp.toLp 2 (starCoord r i)

/-- Coordinates of the regular tetrahedron `{(1,1,1),(1,-1,-1),(-1,1,-1),(-1,-1,1)}/√3`. -/
def simplexCoord : Fin 4 → Fin 3 → ℝ :=
  let p := Real.sqrt (1 / 3)
  ![![p, p, p], ![p, -p, -p], ![-p, p, -p], ![-p, -p, p]]

/-- The regular tetrahedron in `ℝ³`, unit vectors with pairwise inner products `-1/3`. -/
def simplexVec (i : Fin 4) : Sample 3 := WithLp.toLp 2 (simplexCoord i)

theorem gram_starVec {r : ℝ} (h0 : 0 ≤ r) (h1 : r ≤ 1) :
    gram (starVec r) = idealStarCov 4 r := by
  have hq : Real.sqrt ((1 - r ^ 2) / 3) * Real.sqrt ((1 - r ^ 2) / 3) = (1 - r ^ 2) / 3 :=
    Real.mul_self_sqrt (div_nonneg (by nlinarith) (by norm_num))
  ext i j
  simp only [gram, idealStarCov, starVec, starCoord]
  generalize Real.sqrt ((1 - r ^ 2) / 3) = q at hq ⊢
  simp only [PiLp.inner_apply]
  fin_cases i <;> fin_cases j <;>
    simp [Fin.sum_univ_four] <;> norm_num <;> nlinarith [hq]

theorem gram_simplexVec : gram simplexVec = regularSimplexGram 4 := by
  have hp : Real.sqrt (1 / 3) * Real.sqrt (1 / 3) = 1 / 3 :=
    Real.mul_self_sqrt (by norm_num)
  ext i j
  simp only [gram, regularSimplexGram, simplexVec, simplexCoord]
  generalize Real.sqrt (1 / 3) = p at hp ⊢
  simp only [PiLp.inner_apply]
  fin_cases i <;> fin_cases j <;>
    simp [Fin.sum_univ_three] <;> norm_num <;> nlinarith [hp]

theorem measurableSet_frontierEvent (d : ℕ) (τ : ℝ) : MeasurableSet (frontierEvent d τ) := by
  have : frontierEvent d τ =
      {x | τ < x 0} ∩ ⋃ i : Fin (d + 1), ⋃ (_ : i ≠ 0), {x | x i ≤ τ} := by
    ext x; simp [frontierEvent]
  rw [this]
  refine (measurableSet_lt measurable_const (by fun_prop)).inter
    (MeasurableSet.iUnion fun i => MeasurableSet.iUnion fun _ => ?_)
  exact measurableSet_le (by fun_prop) measurable_const

theorem idealStarFn_eq_starVec {r : ℝ} (h0 : 0 ≤ r) (h1 : r ≤ 1) (τ : ℝ) :
    idealStarFn 4 r τ =
      (stdGaussian (Sample 4)).real
        {x | τ < ⟪starVec r 0, x⟫ ∧ ∃ i : Fin 5, i ≠ 0 ∧ ⟪starVec r i, x⟫ ≤ τ} := by
  rw [idealStarFn, ← gram_starVec h0 h1, bridge 4 5 (starVec r) _ (measurableSet_frontierEvent 4 τ)]
  rfl

end T2
end CubicPathwidth

#print axioms CubicPathwidth.T2.bridge
#print axioms CubicPathwidth.T2.gram_posSemidef
#print axioms CubicPathwidth.T2.gram_starVec
#print axioms CubicPathwidth.T2.gram_simplexVec
#print axioms CubicPathwidth.T2.idealStarFn_eq_starVec
Back to top