SourceBlockPathMass.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The source predictor's off-child fractions are bounded by the actual forward path drop. The final ineligible path has drop one even if other children still continue.

theorem OAI.LipschitzHilbert.AngularGrid.sourceBlock_child_fractions line 21
theorem OAI.LipschitzHilbert.AngularGrid.sourceBlock_off_fractions line 43

theorem OAI.LipschitzHilbert.AngularGrid.sourceBlock_continuing_drop line 61

Source documentation

A continuing path selects its actual child cell; its lost fraction pays for every other continuing child and every terminated top.

theorem sourceBlock_continuing_drop {K : ℕ} (g : AngularGrid) (tops : Finset ι)
    (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
    (hp : ∀ t ∈ tops, 0 ≤ precision t) (hw : ∀ t x, 0 < weight t x)
    (hK : 0 < K) (σ : Fin K) (j : ℕ) (top : ι) (htop : top ∈ tops)
    (he : g.eligible cutoff (precision top) (ShiftedBlocks.endpoint σ (j+1))) (x : X)
    (i₀ : g.sourceBlockCells tops slope precision cutoff (ShiftedBlocks.endpoint σ j)
      (ShiftedBlocks.endpoint σ (j+1)) (g.index (ShiftedBlocks.endpoint σ j) (slope top)))
    (hi : i₀.val = g.index (ShiftedBlocks.endpoint σ (j+1)) (slope top)) :
    let n := g.mass tops slope precision cutoff weight (ShiftedBlocks.endpoint σ j)
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.ShiftedBlocks.endpoint

theorem OAI.LipschitzHilbert.AngularGrid.sourceBlock_terminal_drop line 90

Source documentation

At the terminal block any remaining child can serve as the graph's exception: both its complement and its defect are bounded by drop one.

theorem sourceBlock_terminal_drop {K : ℕ} (g : AngularGrid) (tops : Finset ι)
    (slope precision : ι → ℝ) (cutoff : ℝ) (weight : ι → X → ℝ)
    (hp : ∀ t ∈ tops, 0 ≤ precision t) (hw : ∀ t x, 0 < weight t x)
    (hK : 0 < K) (σ : Fin K) (j : ℕ) (top : ι) (htop : top ∈ tops)
    (he : g.eligible cutoff (precision top) (ShiftedBlocks.endpoint σ j))
    (hnext : ¬g.eligible cutoff (precision top) (ShiftedBlocks.endpoint σ (j+1))) (x : X)
    (i₀ : g.sourceBlockCells tops slope precision cutoff (ShiftedBlocks.endpoint σ j)
      (ShiftedBlocks.endpoint σ (j+1)) (g.index (ShiftedBlocks.endpoint σ j) (slope top))) :
    let n := g.mass tops slope precision cutoff weight (ShiftedBlocks.endpoint σ j)
…

Mentions: OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.ShiftedBlocks.endpoint

theorem OAI.LipschitzHilbert.sourcePredictionValue_pos line 119