EventMass.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The quantile event has a positive deficit

Finite sums implement the event calculation in the proof of phase:quantile-gap. The only geometric condition is the explicitly proved fact that a resonant completion of the event lies below its chosen central interval.

def OAI.LipschitzHilbert.PhaseCombinatorics.rectangularEvent line 24
theorem OAI.LipschitzHilbert.PhaseCombinatorics.independent_rectangular_event line 27
theorem OAI.LipschitzHilbert.PhaseCombinatorics.restricted_marginal_sum_le line 35

theorem OAI.LipschitzHilbert.PhaseCombinatorics.projected_rectangular_event_le line 48

Source documentation

Forcing the missing coordinate into J bounds the projected event by the independent mass of I × K × J.

theorem projected_rectangular_event_le {frequency : ι → ℝ} {gap : ℝ}
    (hgap : 0 < gap) (hsep : Separated frequency gap) (x : ι → ℝ)
    (hx : ∀ i, 0 ≤ x i) (I K L J : Finset ι)
    (hcompletion : ∀ i ∈ I, ∀ k ∈ K, ∀ l ∈ L, ∀ j,
      Resonant frequency gap i j k l → j ∈ J) :
    (∑ q ∈ rectangularEvent I K L, projectedMass frequency gap x q) ≤
      (∑ i ∈ I, x i) * (∑ k ∈ K, x k) * (∑ j ∈ J, x j) := by
…

Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Separated, OAI.LipschitzHilbert.PhaseCombinatorics.Resonant, OAI.LipschitzHilbert.PhaseCombinatorics.rectangularEvent, OAI.LipschitzHilbert.PhaseCombinatorics.projectedMass

theorem OAI.LipschitzHilbert.PhaseCombinatorics.rectangular_event_deficit line 92

Source documentation

When J ⊆ L, the independent mass in L \ J is a definite event deficit. This is the exact finite form of the manuscript's calculation.

theorem rectangular_event_deficit {frequency : ι → ℝ} {gap : ℝ}
    (hgap : 0 < gap) (hsep : Separated frequency gap) (x : ι → ℝ)
    (hx : ∀ i, 0 ≤ x i) (I K L J : Finset ι) (hJL : J ⊆ L)
    (hcompletion : ∀ i ∈ I, ∀ k ∈ K, ∀ l ∈ L, ∀ j,
      Resonant frequency gap i j k l → j ∈ J) :
    (∑ i ∈ I, x i) * (∑ k ∈ K, x k) * (∑ l ∈ L \ J, x l) ≤
      ∑ q ∈ rectangularEvent I K L,
        (independentMass x q - projectedMass frequency gap x q) := by
…

theorem OAI.LipschitzHilbert.PhaseCombinatorics.threshold_event_completion line 108

Source documentation

The source's frequency-threshold event satisfies the preceding completion condition. Strict inequality on J leaves both endpoints of [e,h] in L \ J.

theorem threshold_event_completion {frequency : ι → ℝ} {gap a b e h : ℝ}
    (hgap : 0 < gap) (hab : gap ≤ b - a) (heh : h - e ≤ (b - a) / 2) :
    ∀ i ∈ Finset.univ.filter (fun i => b ≤ frequency i),
      ∀ k ∈ Finset.univ.filter (fun k => frequency k ≤ a),
      ∀ l ∈ Finset.univ.filter (fun l => frequency l ≤ h), ∀ j,
        Resonant frequency gap i j k l →
          j ∈ Finset.univ.filter (fun j => frequency j < e) := by
…

Mentions: OAI.LipschitzHilbert.PhaseCombinatorics.Resonant

theorem OAI.LipschitzHilbert.PhaseCombinatorics.quantitative_gap_of_event_mass_bounds line 121

Source documentation

The exact quantitative constant obtained from two quarter-tail masses and a half of the central mass. Quantile existence supplies these hypotheses.

theorem quantitative_gap_of_event_mass_bounds {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)
    (I K L J : Finset ι) (hJL : J ⊆ L)
    (hcompletion : ∀ i ∈ I, ∀ k ∈ K, ∀ l ∈ L, ∀ j,
      Resonant frequency gap i j k l → j ∈ J)
    (hI : κ / 4 ≤ ∑ i ∈ I, x i) (hK : κ / 4 ≤ ∑ k ∈ K, x k)
    (hcentral : (1 - κ / 2) / 2 ≤ ∑ l ∈ L \ J, x l) :
    resonanceSum frequency gap x ≤ 1 - κ ^ 4 * (1 - κ / 2) ^ 2 / 4096 := by
…

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