IntervalSegmentCharging.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Unary segments may charge whole disjoint drop intervals. This includes completed segments directly, without replacing their drops by single steps.

theorem OAI.LipschitzHilbert.interval_charged_segment_shell_card line 19

Source documentation

A whole completed segment, or the interruption charged by a remainder, provides a fixed positive drop. Pairwise disjoint charge intervals give the same shell count as single-step charges, including one final uncharged piece.

theorem interval_charged_segment_shell_card {ι : Type*} [Fintype ι]
    (mass : ι → ℝ) (charge : ι → Option (ℕ × ℕ)) (n : ℕ → ℝ)
    (hn : Antitone n)
    (hnone : ∀ i j, charge i = none → charge j = none → i = j)
    (hdisjoint : ∀ i j a b c d, i ≠ j → charge i = some (a,b) →
      charge j = some (c,d) → b ≤ c ∨ d ≤ a)
    {drop lo hi : ℝ} (hdrop : 0 < drop) (hlohi : lo ≤ hi)
    (hcharge : ∀ i a b, charge i = some (a,b) →
      mass i - 2 ≤ n a ∧ n a ≤ mass i ∧ drop ≤ n a - n b)
    (S : Finset ι) (hS : ∀ i ∈ S, lo ≤ mass i ∧ mass i ≤ hi) :
    (S.card : ℝ) ≤ 2 + (hi - lo + 2) / drop := by
…

theorem OAI.LipschitzHilbert.interval_charged_segment_weight_sum line 78