SegmentCharging.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Charging unary segments to positive mass drops

This is the finite counting argument in §10 res:segment-shell-count. Completed segments charge their starting drop, and remainders charge the next interruption. The charge can lie at most two units of mass below the segment start. Injectivity permits one final uncharged segment.

theorem OAI.LipschitzHilbert.charged_segment_shell_card line 24

Source documentation

An injective optional charge permits one final remainder and no multiplicity depending on the number of unary levels.

theorem charged_segment_shell_card {ι : Type*} [Fintype ι]
    (mass : ι → ℝ) (charge : ι → Option ℕ) (n : ℕ → ℝ)
    (hn : Antitone n) (hinj : Function.Injective charge)
    {c a b : ℝ} (hc : 0 < c) (hab : a ≤ b)
    (hcharge : ∀ i k, charge i = some k →
      mass i - 2 ≤ n k ∧ n k ≤ mass i ∧ c ≤ n k - n (k + 1))
    (S : Finset ι) (hS : ∀ i ∈ S, a ≤ mass i ∧ mass i ≤ b) :
    (S.card : ℝ) ≤ 2 + (b - a + 2) / c := by
…

theorem OAI.LipschitzHilbert.charged_segment_shell_linear line 78

Source documentation

A ratio-sixteen shell has a linear cardinal bound with an absolute coefficient depending only on the fixed minimum interruption drop.

theorem charged_segment_shell_linear {ι : Type*} [Fintype ι]
    (mass : ι → ℝ) (charge : ι → Option ℕ) (n : ℕ → ℝ)
    (hn : Antitone n) (hinj : Function.Injective charge)
    {c t : ℝ} (hc : 0 < c) (ht : 1 ≤ t)
    (hcharge : ∀ i k, charge i = some k →
      mass i - 2 ≤ n k ∧ n k ≤ mass i ∧ c ≤ n k - n (k + 1))
    (S : Finset ι) (hS : ∀ i ∈ S, t ≤ mass i ∧ mass i ≤ 16 * t) :
    (S.card : ℝ) ≤ (2 + 17 / c) * t := by
…