Projection.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Projection of the near-resonant quadruple measure

The quantile-gap argument in §7 projects the triple weight on quadruples to coordinates (i,k,l). Unique completion makes the Hellinger affinity of the projected measures exactly the affinity before projection.

abbrev OAI.LipschitzHilbert.PhaseCombinatorics.Triple line 22
def OAI.LipschitzHilbert.PhaseCombinatorics.insertSecond line 24
def OAI.LipschitzHilbert.PhaseCombinatorics.projectedMass line 30
def OAI.LipschitzHilbert.PhaseCombinatorics.independentMass line 34

theorem OAI.LipschitzHilbert.PhaseCombinatorics.resonant_event_completion_lt line 38

Source documentation

The quantile event forces its resonant completion below the selected central half interval. This is the geometric step behind the event deficit.

theorem resonant_event_completion_lt {frequency : ι → ℝ} {gap a b e h : ℝ}
    (hgap : 0 < gap) (hab : gap ≤ b - a) (heh : h - e ≤ (b - a) / 2)
    {i j k l : ι} (hr : Resonant frequency gap i j k l)
    (hi : b ≤ frequency i) (hk : frequency k ≤ a) (hl : frequency l ≤ h) :
    frequency j < e := by
…

Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Resonant

theorem OAI.LipschitzHilbert.PhaseCombinatorics.projectedMass_nonneg line 46
theorem OAI.LipschitzHilbert.PhaseCombinatorics.independentMass_nonneg line 51
theorem OAI.LipschitzHilbert.PhaseCombinatorics.sum_projectedMass_eq line 55
theorem OAI.LipschitzHilbert.PhaseCombinatorics.sum_projectedMass_le_one line 64
theorem OAI.LipschitzHilbert.PhaseCombinatorics.sum_independentMass_eq_one line 72

theorem OAI.LipschitzHilbert.PhaseCombinatorics.sqrt_sum_mul_of_unique_support line 79

Source documentation

With at most one nonzero summand, taking this square root commutes with the sum exactly.

theorem sqrt_sum_mul_of_unique_support [Fintype ι] (a : ι → ℝ) (b : ℝ)
    (hunique : ∀ i j, a i ≠ 0 → a j ≠ 0 → i = j) :
    Real.sqrt ((∑ i, a i) * b) = ∑ i, Real.sqrt (a i * b) := by
…

theorem OAI.LipschitzHilbert.PhaseCombinatorics.marginal_unique_support line 101
theorem OAI.LipschitzHilbert.PhaseCombinatorics.marginal_mul_permuted_eq_independent line 114
theorem OAI.LipschitzHilbert.PhaseCombinatorics.projected_affinity_eq line 128
Source documentation
The projection preserves the affinity, because each projected point has at most one possible resonant completion.
```
theorem projected_affinity_eq [Fintype ι]
    {frequency : ι → ℝ} {gap : ℝ} (hgap : 0 < gap)
    (hsep : Separated frequency gap) (x : ι → ℝ) :
    (∑ q : Triple ι,
      Real.sqrt (projectedMass frequency gap x q * independentMass x q)) =
      ∑ q : Quadruple ι, Real.sqrt
        (marginal frequency gap x q * marginal frequency gap x (swapPairs q)) := by
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.PhaseCombinatorics.Triple, OAI.LipschitzHilbert.PhaseCombinatorics.projectedMass, OAI.LipschitzHilbert.PhaseCombinatorics.independentMass, OAI.LipschitzHilbert.PhaseCombinatorics.Quadruple, OAI.LipschitzHilbert.PhaseCombinatorics.marginal, OAI.LipschitzHilbert.PhaseCombinatorics.swapPairs
theorem OAI.LipschitzHilbert.PhaseCombinatorics.resonanceSum_nonneg line 159
theorem OAI.LipschitzHilbert.PhaseCombinatorics.resonanceSum_sq_le_projected_affinity line 165
Source documentation
The bound in exactly the affinity convention used for finite probabilities.
```
theorem resonanceSum_sq_le_projected_affinity [Fintype ι]
    {frequency : ι → ℝ} {gap : ℝ} (hgap : 0 < gap)
    (hsep : Separated frequency gap) (x : ι → ℝ)
    (hx : ∀ i, 0 ≤ x i) (hsum : ∑ i, x i = 1) :
    resonanceSum frequency gap x ^ 2 ≤
      affinity (projectedMass frequency gap x) (independentMass x) := by
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.PhaseCombinatorics.resonanceSum, OAI.LipschitzHilbert.affinity, OAI.LipschitzHilbert.PhaseCombinatorics.projectedMass, OAI.LipschitzHilbert.PhaseCombinatorics.independentMass
theorem OAI.LipschitzHilbert.PhaseCombinatorics.resonanceSum_gap_of_event_deficit line 185
Source documentation
Any event with a definite deficit between the projected and independent triple laws gives the quantitative improvement in the fourth-moment sum.
```
theorem resonanceSum_gap_of_event_deficit [Fintype ι]
    {frequency : ι → ℝ} {gap : ℝ} (hgap : 0 < gap)
    (hsep : Separated frequency gap) (x : ι → ℝ)
    (hx : ∀ i, 0 ≤ x i) (hsum : ∑ i, x i = 1)
    (s : Finset (Triple ι)) {g : ℝ} (hg : 0 ≤ g)
    (hdeficit : g ≤ ∑ q ∈ s,
      (independentMass x q - projectedMass frequency gap x q)) :
    resonanceSum frequency gap x ≤ 1 - g ^ 2 / 4 := by
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.PhaseCombinatorics.Triple, OAI.LipschitzHilbert.PhaseCombinatorics.independentMass, OAI.LipschitzHilbert.PhaseCombinatorics.projectedMass, OAI.LipschitzHilbert.PhaseCombinatorics.resonanceSum