QuantileGap.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Quantitative fourth-moment gap

The complete combinatorial lemma phase:quantile-gap in §7 of A uniform Hilbert transform estimate for Lipschitz directions. This is a supporting lemma, not the paper's main Hilbert-transform theorem.

theorem OAI.LipschitzHilbert.PhaseCombinatorics.separated_injective line 21

theorem OAI.LipschitzHilbert.PhaseCombinatorics.quantile_gap line 30

Source documentation

The precise strict gap, uniform in the number and positions of frequencies.

theorem quantile_gap [Fintype ι] {frequency : ι → ℝ} {gap κ : ℝ}
    (hgap : 0 < gap) (hsep : Separated frequency gap)
    (hκ : 0 < κ) (hκ1 : κ < 1) (x : ι → ℝ)
    (hx : ∀ i, 0 ≤ x i) (hsum : ∑ i, x i = 1)
    (hatom : ∀ i, x i ≤ 1 - κ) :
    resonanceSum frequency gap x ≤ 1 - κ ^ 4 * (1 - κ / 2) ^ 2 / 4096 := by
…

Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.PhaseCombinatorics.resonanceSum

theorem OAI.LipschitzHilbert.PhaseCombinatorics.quantile_gap_simplified line 70

Source documentation

The simplified numerical lower bound for the gap in the manuscript.

theorem quantile_gap_simplified [Fintype ι] {frequency : ι → ℝ} {gap κ : ℝ}
    (hgap : 0 < gap) (hsep : Separated frequency gap)
    (hκ : 0 < κ) (hκ1 : κ < 1) (x : ι → ℝ)
    (hx : ∀ i, 0 ≤ x i) (hsum : ∑ i, x i = 1)
    (hatom : ∀ i, x i ≤ 1 - κ) :
    resonanceSum frequency gap x ≤ 1 - κ ^ 4 / 16384 := by
…

Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.PhaseCombinatorics.resonanceSum