OAI/Analysis/LipschitzHilbert/Trees/UnaryRunCharging.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Charge completed unary segments to themselves and remainders to the next genuine interruption. The final path remainder is the only exception.

  1. abbrev OAI.LipschitzHilbert.UnaryRunSegment line 18
  2. def OAI.LipschitzHilbert.unaryRunCharge line 20
  3. theorem OAI.LipschitzHilbert.runSegment_eq line 25
  4. theorem OAI.LipschitzHilbert.unaryRunCharge_none line 35
  5. theorem OAI.LipschitzHilbert.unaryRunCharge_some line 44
  6. theorem OAI.LipschitzHilbert.unaryRunCharge_none_unique line 58
  7. theorem OAI.LipschitzHilbert.unaryRunCharge_bounds line 65
  8. theorem OAI.LipschitzHilbert.unaryRunCharge_disjoint line 75
  9. theorem OAI.LipschitzHilbert.unaryRunCharge_mass_drop line 107
  10. theorem OAI.LipschitzHilbert.unary_runs_weight_sum line 126

    Source documentation

    All actual unary runs share one charged weight bound. Completed segments pay their own drops, and every nonfinal remainder pays the next interruption. There is only one uncharged final remainder on the path.

    theorem unary_runs_weight_sum (hn : Antitone n) {c M μ : ℝ}
    (hc : 0 < c) (hc1 : c ≤ 1) (hM : 1 ≤ M) (hμ : μ ≤ 1 / 12)
    (hmass : ∀ i : UnaryRunSegment R P, M ≤ n i.2.val.1)
    (hinterruption : ∀ j, start ≤ j → j < finish → ¬ unary j → c ≤ n j - n (j + 1)) :
    (∑ i : UnaryRunSegment R P, (n i.2.val.1) ^ ((-1 + μ) * (3 / 2 : ℝ))) ≤
      2 * (2 + 17 / c) * M ^ (-(1 / 2 : ℝ) + 3 * μ / 2) := by
…

    Mentions: OAI.LipschitzHilbert.UnaryRunSegment

  11. theorem OAI.LipschitzHilbert.exists_unary_runs_weighted_partition line 140

    Source documentation

    Construct the runs and their greedy segments directly from the unary predicate and masses, then obtain the global negative-power weight bound.

    theorem exists_unary_runs_weighted_partition (hn : Antitone n)
    (horder : start ≤ finish) {c M μ : ℝ}
    (hc : 0 < c) (hc1 : c ≤ 1) (hM : 1 ≤ M) (hμ : μ ≤ 1 / 12)
    (hsmall : ∀ j, start ≤ j → j < finish → unary j → n j - n (j + 1) < 1)
    (hmass : ∀ j, start ≤ j → j < finish → unary j → M ≤ n j)
    (hinterruption : ∀ j, start ≤ j → j < finish → ¬ unary j → c ≤ n j - n (j + 1)) :
    ∃ R : UnaryRunPartition unary start finish,
      ∃ P : ∀ r : R.runs, UnarySegmentPartition n r.val.1 r.val.2,
        (∑ i : UnaryRunSegment R P, (n i.2.val.1) ^ ((-1 + μ) * (3 / 2 : ℝ))) ≤
          2 * (2 + 17 / c) * M ^ (-(1 / 2 : ℝ) + 3 * μ / 2) := by
…

    Mentions: OAI.LipschitzHilbert.UnaryRunPartition, OAI.LipschitzHilbert.UnarySegmentPartition, OAI.LipschitzHilbert.UnaryRunSegment