MarkedShells.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Marked mass shells

The shell estimate and weighted sum of §10, res:marked-shell-count and res:marked-weight-sum. A positive drop at every marked index makes the corresponding masses separated. We use shells of ratio four, grouping pairs of the manuscript's dyadic shells, so that the geometric ratio is at most one half throughout the required exponent range.

theorem OAI.LipschitzHilbert.marked_mass_separated line 26
theorem OAI.LipschitzHilbert.separated_shell_card line 43
theorem OAI.LipschitzHilbert.four_rpow_le_half line 55

theorem OAI.LipschitzHilbert.separated_negative_power_sum line 65

Source documentation

A separated finite family above M has a summable negative-power weight, uniformly in its cardinality and its largest mass.

theorem separated_negative_power_sum {ι : Type*} [Fintype ι]
    (mass : ι → ℝ) {c M e : ℝ} (hc : 0 < c) (hM : 1 ≤ M)
    (he : e ≤ -(3 / 2 : ℝ)) (hsep : Separated mass c)
    (hmass : ∀ i, M ≤ mass i) :
    (∑ i, mass i ^ e) ≤ 2 * (1 + 3 / c) * M ^ (e + 1) := by
…

theorem OAI.LipschitzHilbert.marked_weight_sum line 143

Source documentation

The manuscript's marked weight bound follows from the actual positive mass drops, with an explicit constant depending only on c.

theorem marked_weight_sum (n : ℕ → ℝ) (hn : Antitone n) (S : Finset ℕ)
    {c M μ : ℝ} (hc : 0 < c) (hM : 1 ≤ M) (hμ : μ ≤ 1 / 12)
    (hdrop : ∀ i ∈ S, c ≤ n i - n (i + 1)) (hmass : ∀ i ∈ S, M ≤ n i) :
    (∑ i ∈ S, n i ^ (-2 + 2 * μ)) ≤
      2 * (1 + 3 / c) * M ^ (-1 + 2 * μ) := by
…