SourcePredictableLength.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Packets surviving a child level have the original horizontal length needed by the unconditional derivative estimate on its averaging cell.

theorem OAI.LipschitzHilbert.AngularGrid.source_eligible_length_lower line 11

theorem OAI.LipschitzHilbert.SourceLabeledLattice.source_stopping_length_lower line 35

Source documentation

The stopping level is the actual last eligible level of the original packet length; surviving it implies the predictable-length lower bound.

theorem source_stopping_length_lower (P : SourceLabeledLattice N κ Label Item)
    (g : AngularGrid) {w B : ℝ} (hw : 0 < w) (hB : 0 < B)
    (hzero : ∀ j, g.eligible (g.rootWidth/B^2) (w/P.length j) 0)
    (level : ℕ) (j : Fin N)
    (hstop : level ≤ g.lastEligible (g.rootWidth/B^2) (w/P.length j)
      (div_pos hw (P.length_pos j))) :
    B^2*w/g.width level ≤ P.length j := by
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice, OAI.LipschitzHilbert.AngularGrid