PhaseCombinatorics.lean`

27 declarations, 0 contain sorry, 0 declared as axioms

Finite-phase resonance combinatorics

These are the elementary finite combinatorial ingredients of §7, Lemma phase:quantile-gap, of A uniform Hilbert transform estimate for Lipschitz directions. The frequency separation is quantitative; no assumption about additive independence is made.

def OAI.LipschitzHilbert.PhaseCombinatorics.Separated line 27
def OAI.LipschitzHilbert.PhaseCombinatorics.Resonant line 30
theorem OAI.LipschitzHilbert.PhaseCombinatorics.resonant_swap_left line 33
theorem OAI.LipschitzHilbert.PhaseCombinatorics.resonant_swap_right line 37
theorem OAI.LipschitzHilbert.PhaseCombinatorics.resonant_swap_pairs line 41
theorem OAI.LipschitzHilbert.PhaseCombinatorics.unique_fourth line 49
Source documentation
Three fixed indices determine at most one fourth index.
```
theorem unique_fourth {frequency : ι → ℝ} {gap : ℝ}
    (hgap : 0 < gap) (hsep : Separated frequency gap)
    {i j k l l' : ι} (h : Resonant frequency gap i j k l)
    (h' : Resonant frequency gap i j k l') : l = l' := by
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.PhaseCombinatorics.Resonant
theorem OAI.LipschitzHilbert.PhaseCombinatorics.unique_third line 62
theorem OAI.LipschitzHilbert.PhaseCombinatorics.unique_second line 68
theorem OAI.LipschitzHilbert.PhaseCombinatorics.unique_first line 74
theorem OAI.LipschitzHilbert.PhaseCombinatorics.sum_completions_le line 82
Source documentation
For three fixed indices, summing a nonnegative weight over resonant completions costs at most that weight.
```
theorem sum_completions_le [Fintype ι] {frequency : ι → ℝ} {gap : ℝ}
    (hgap : 0 < gap) (hsep : Separated frequency gap)
    (i j k : ι) (a : ℝ) (ha : 0 ≤ a) :
    (∑ l, if Resonant frequency gap i j k l then a else 0) ≤ a := by
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.PhaseCombinatorics.Resonant
theorem OAI.LipschitzHilbert.PhaseCombinatorics.resonance_triple_mass_le_one line 107
Source documentation
Each triple-coordinate marginal used in the fourth-moment argument has total mass at most one. This is the first marginal, omitting the fourth coordinate.
```
theorem resonance_triple_mass_le_one [Fintype ι]
    {frequency : ι → ℝ} {gap : ℝ} (hgap : 0 < gap)
    (hsep : Separated frequency gap) (x : ι → ℝ)
    (hx : ∀ i, 0 ≤ x i) (hsum : ∑ i, x i = 1) :
    (∑ i, ∑ j, ∑ k, ∑ l,
      if Resonant frequency gap i j k l then x i * x j * x k else 0) ≤ 1 := by
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.PhaseCombinatorics.Resonant
abbrev OAI.LipschitzHilbert.PhaseCombinatorics.Quadruple line 128
def OAI.LipschitzHilbert.PhaseCombinatorics.swapPairs line 130
def OAI.LipschitzHilbert.PhaseCombinatorics.swapLast line 136
def OAI.LipschitzHilbert.PhaseCombinatorics.marginal line 143
Source documentation
The first of the four triple-coordinate subprobability weights.
```
def marginal (frequency : ι → ℝ) (gap : ℝ) (x : ι → ℝ) (q : Quadruple ι) : ℝ :=
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Quadruple
theorem OAI.LipschitzHilbert.PhaseCombinatorics.marginal_nonneg line 147
theorem OAI.LipschitzHilbert.PhaseCombinatorics.marginal_mass_le_one line 154
theorem OAI.LipschitzHilbert.PhaseCombinatorics.permuted_marginal_mass_le_one line 163
Source documentation
Reindexing gives all four subprobability bounds without further losses.
```
theorem permuted_marginal_mass_le_one [Fintype ι]
    {frequency : ι → ℝ} {gap : ℝ} (hgap : 0 < gap)
    (hsep : Separated frequency gap) (x : ι → ℝ)
    (hx : ∀ i, 0 ≤ x i) (hsum : ∑ i, x i = 1)
    (e : Quadruple ι ≃ Quadruple ι) :
    (∑ q : Quadruple ι, marginal frequency gap x (e q)) ≤ 1 := by
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.PhaseCombinatorics.Quadruple, OAI.LipschitzHilbert.PhaseCombinatorics.marginal

theorem OAI.LipschitzHilbert.PhaseCombinatorics.affinity_le_one line 173

Source documentation

The elementary affinity bound for two subprobabilities.

theorem affinity_le_one [Fintype ι] (a b : ι → ℝ)
    (ha : ∀ i, 0 ≤ a i) (hb : ∀ i, 0 ≤ b i)
    (hsa : ∑ i, a i ≤ 1) (hsb : ∑ i, b i ≤ 1) :
    (∑ i, Real.sqrt (a i * b i)) ≤ 1 := by
…

theorem OAI.LipschitzHilbert.PhaseCombinatorics.geometric_sum_sq_le_affinity line 192

Source documentation

Four-factor Hölder in the form used by the quantile argument: the square of the geometric sum is bounded by the affinity of its first two weights.

theorem geometric_sum_sq_le_affinity [Fintype ι] (a b c d : ι → ℝ)
    (hc : ∀ i, 0 ≤ c i) (hd : ∀ i, 0 ≤ d i)
    (hsc : ∑ i, c i ≤ 1) (hsd : ∑ i, d i ≤ 1) :
    (∑ i, Real.sqrt (Real.sqrt (a i * b i) * Real.sqrt (c i * d i))) ^ 2 ≤
      ∑ i, Real.sqrt (a i * b i) := by
…

def OAI.LipschitzHilbert.PhaseCombinatorics.geometricTerm line 222
theorem OAI.LipschitzHilbert.PhaseCombinatorics.geometricTerm_eq line 231
Source documentation
The four triple-coordinate weights have geometric mean (xᵢ xⱼ xₖ xₗ)^(3/4), written with square roots.
```
theorem geometricTerm_eq {frequency : ι → ℝ} {gap : ℝ} {x : ι → ℝ}
    (hx : ∀ i, 0 ≤ x i) (i j k l : ι) :
    geometricTerm frequency gap x (i, j, k, l) =
      if Resonant frequency gap i j k l then
        Real.sqrt (Real.sqrt ((x i * x j * x k * x l) ^ 3)) else 0 := by
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.geometricTerm, OAI.LipschitzHilbert.PhaseCombinatorics.Resonant
theorem OAI.LipschitzHilbert.PhaseCombinatorics.sqrt_sqrt_cube_eq_rpow line 251
theorem OAI.LipschitzHilbert.PhaseCombinatorics.geometricTerm_eq_rpow line 257
def OAI.LipschitzHilbert.PhaseCombinatorics.resonanceSum line 268
Source documentation
The ordinary fourth-moment quantity in the manuscript.
```
def resonanceSum [Fintype ι] (frequency : ι → ℝ) (gap : ℝ) (x : ι → ℝ) : ℝ :=
…
```
theorem OAI.LipschitzHilbert.PhaseCombinatorics.resonanceSum_sq_le_affinity line 272
Source documentation
The affinity inequality that precedes the strict quantile deficit.
```
theorem resonanceSum_sq_le_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 ≤
      ∑ q : Quadruple ι, Real.sqrt
        (marginal frequency gap x q * marginal frequency gap x (swapPairs q)) := by
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.PhaseCombinatorics.resonanceSum, OAI.LipschitzHilbert.PhaseCombinatorics.Quadruple, OAI.LipschitzHilbert.PhaseCombinatorics.marginal, OAI.LipschitzHilbert.PhaseCombinatorics.swapPairs
theorem OAI.LipschitzHilbert.PhaseCombinatorics.resonanceSum_le_one line 286
Source documentation
The usual constant-one fourth-moment bound, before its strict improvement.
```
theorem resonanceSum_le_one [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 ≤ 1 := by
…
```
Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.PhaseCombinatorics.resonanceSum