SourceSnapshotAmplitudeScale.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual concentration bound n <= N L^C supplies the amplitude scale used in the marked prediction, with no extra mass-size premise.

theorem OAI.LipschitzHilbert.source_concentration_phase_power line 14
Source documentation
Raising the concentration mass bound to a phase in [0,1] preserves its fixed polynomial factor and the manuscript's single power N^mu.
```
theorem source_concentration_phase_power {L N n C μ : ℝ}
    (hL : 1 ≤ L) (hN : 0 < N) (hn : 0 < n) (hC : 0 ≤ C)
    (hμ0 : 0 ≤ μ) (hμ1 : μ ≤ 1) (hmass : n ≤ L^C*N) :
    n^μ ≤ L^C*(1+N^μ) := by
…
```

theorem OAI.LipschitzHilbert.source_snapshot_amplitude_scale line 30

Source documentation

Both mass and node-size premises of the source predictor follow with C_* = C + Q from the concentration and actual node-amplitude bounds.

theorem source_snapshot_amplitude_scale {L N n C Q μ : ℝ}
    (hL : 1 ≤ L) (hN : 0 < N) (hn : 0 < n) (hC : 0 ≤ C) (hQ : 0 ≤ Q)
    (hμ0 : 0 ≤ μ) (hμ1 : μ ≤ 1) (hmass : n ≤ L^C*N) :
    n^μ ≤ L^(Q+C)*(1+N^μ) ∧ L^Q*n^μ ≤ L^(Q+C)*(1+N^μ) := by
…