SourceResidualBlockBudget.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's rounded block parameters bound the number of residual lengths polynomially, uniformly over the packet family.

theorem OAI.LipschitzHilbert.eventually_source_block_length_budget line 17
Source documentation
The actual integer exponent of the source branching is at most L² for large L; no bound depends on the number of packet scales.
```
theorem eventually_source_block_length_budget :
    ∀ᶠ L : ℝ in atTop,
      ((SourceParameters.stepExponent L*SourceParameters.blockCount L:ℕ):ℝ) ≤ L^(2:ℝ) := by
…
```
Mentions: OAI.LipschitzHilbert.SourceParameters.stepExponent, OAI.LipschitzHilbert.SourceParameters.blockCount

theorem OAI.LipschitzHilbert.SourceLabeledLattice.eventually_shifted_residual_length_budget line 45

Source documentation

Every shifted residual block of an actual dyadic packet family has at most L² lengths for sufficiently large L.

theorem eventually_shifted_residual_length_budget :
    ∀ᶠ L : ℝ in atTop,
    ∀ (N : ℕ) (κ : Type) (Label : Fin N → Type) (Item : ∀ j, Label j → Type)
      [Fintype κ] [∀ j l, Fintype (Item j l)]
      (P : SourceLabeledLattice N κ Label Item) (grid : AngularGrid),
      (grid.branching:ℝ) = SourceParameters.step L →
    ∀ (_hK : 0 < SourceParameters.blockCount L) (shift : Fin (SourceParameters.blockCount L))
      (w : ℝ) (hw : 0 < w),
      (∀ j : Fin N, grid.eligible (grid.rootWidth/(SourceParameters.branching L)^2)
        (w/P.length j) 0) →
    ∀ block : ℕ,
      let stop := fun j : Fin N => grid.lastEligible
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice, OAI.LipschitzHilbert.AngularGrid, OAI.LipschitzHilbert.SourceParameters.step, OAI.LipschitzHilbert.SourceParameters.blockCount, OAI.LipschitzHilbert.SourceParameters.branching