SourceSupportedBandStops.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Clipping a band's stopping level changes no packet when that band has no items. This permits itemwise shortness in every later motion bound.

theorem OAI.LipschitzHilbert.AngularGrid.sourceBandAmplitude_clip_stop line 15

theorem OAI.LipschitzHilbert.AngularGrid.source_length_stop_le_of_item line 40

Source documentation

The actual eligibility stop is bounded whenever an item exists.

theorem source_length_stop_le_of_item (g : AngularGrid)
    (tops : Finset ι) (T : ι → SlopeBox) (P : ι → SourceLabeledLattice N κ Label Item)
    (w cut : ℝ) (hw : 0 < w) (M : ι → ℕ)
    (hzero : ∀ t ∈ tops, ∀ j, g.eligible cut (w/(P t).length j) 0)
    (hshort : ∀ t ∈ tops, ∀ j (l : (P t).labels j) (_u : Item j l),
      (P t).length j ≤ (T t).length)
    (hmax : ∀ t ∈ tops, ∀ k, g.eligible cut (w/(T t).length) k → k ≤ M t)
    (t : ι) (ht : t ∈ tops) (j : Fin N) (l : (P t).labels j) (u : Item j l) :
    g.lastEligible cut (w/(P t).length j) (div_pos hw ((P t).length_pos j)) ≤ M t := by
…

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