SegmentMassSum.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The unary-segment negative-power weight sum in §10 res:segment-weight-sum. Ratio-sixteen shells give geometric ratio at most one half for every exponent used by the manuscript.

theorem OAI.LipschitzHilbert.sixteen_rpow_le_half line 15

theorem OAI.LipschitzHilbert.finite_shell_power_sum line 31

Source documentation

Finite shell summation from a linear shell-cardinality estimate. The bound is independent of the number of populated shells.

theorem finite_shell_power_sum {ι : Type*} [Fintype ι]
    (mass : ι → ℝ) {M C e : ℝ} (hM : 1 ≤ M) (hC : 0 ≤ C)
    (he : e ≤ -(5 / 4 : ℝ)) (hmass : ∀ i, M ≤ mass i)
    (hcount : ∀ (t : ℝ) (S : Finset ι), M ≤ t →
      (∀ i ∈ S, t ≤ mass i ∧ mass i ≤ 16 * t) → (S.card : ℝ) ≤ C * t) :
    (∑ i, mass i ^ e) ≤ 2 * C * M ^ (e + 1) := by
…

theorem OAI.LipschitzHilbert.charged_segment_weight_sum line 100

Source documentation

The exact 3/2 weight exponent needed by Hölder against the good-path cubic variation bound, with its shell hypothesis discharged by charges.

theorem charged_segment_weight_sum {ι : Type*} [Fintype ι]
    (mass : ι → ℝ) (charge : ι → Option ℕ) (n : ℕ → ℝ)
    (hn : Antitone n) (hinj : Function.Injective charge)
    {c M μ : ℝ} (hc : 0 < c) (hM : 1 ≤ M) (hμ : μ ≤ 1 / 12)
    (hmass : ∀ i, M ≤ mass i)
    (hcharge : ∀ i k, charge i = some k →
      mass i - 2 ≤ n k ∧ n k ≤ mass i ∧ c ≤ n k - n (k + 1)) :
    (∑ i, mass i ^ ((-1 + μ) * (3 / 2 : ℝ))) ≤
      2 * (2 + 17 / c) * M ^ (-(1 / 2 : ℝ) + 3 * μ / 2) := by
…