SourceGridParameters.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The source prediction scale gives one uniform marked-cell error in both branches. The only mesh hypothesis is the explicit carrier oscillation bound on a cell; the averaging measure and its remainder are already proved.

theorem OAI.LipschitzHilbert.source_grid_cost_le line 18
theorem OAI.LipschitzHilbert.eventually_source_balanced_grid_parameters line 31
Source documentation
The balanced source factor has a normalized, measurable cell-constant majorant with pointwise error G^(-1/32) * u at the actual parameters.
```
theorem eventually_source_balanced_grid_parameters (C F : ℝ)
    (hC : 0 ≤ C) (hF : 0 ≤ F) :
    ∀ᶠ L : ℝ in atTop, ∀ D N : ℝ,
      1 ≤ D → 0 < N → Real.log N ≤ 2*L →
      let p := Real.sqrt L
…
```
theorem OAI.LipschitzHilbert.eventually_source_dominant_grid_parameters line 123
Source documentation
The unshrunk path vector in the dominant branch has the same final marked-cell error as the balanced branch. All phase and mass hypotheses remain the explicit local estimates proved for the original packets.
```
theorem eventually_source_dominant_grid_parameters (C F : ℝ)
    (hC : 0 ≤ C) (hF : 0 ≤ F) :
    ∀ᶠ L : ℝ in atTop, ∀ D N : ℝ,
      1 ≤ D → 0 < N → Real.log N ≤ 2*L →
      let p := Real.sqrt L
…
```