MomentLevels.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The prescribed retained level in the first paper's moment-batch construction. Its definition counts bad positive integer levels. Monotonicity makes those levels an initial segment, so one plus their cardinal is a good level. The moment convergence hypotheses here are explicit internal proof inputs.

theorem OAI.SLEExactGauge.Target.batchLevel_ge_one line 18
theorem OAI.SLEExactGauge.Target.finite_bad_moment_levels line 23
theorem OAI.SLEExactGauge.Target.finiteMoment_batchLevel_gt line 39
Source documentation
The actual Target.batchLevel, not a separately chosen large level, retains more than three quarters of the limiting moment.
```
theorem finiteMoment_batchLevel_gt (κ : ℝ) (W : WienerLaw) (n : ℕ)
    (hmono : Monotone (fun j : ℕ => finiteMoment κ W n j))
    (hm : 0 < moment κ W n)
    (hlim : Tendsto (fun j : ℕ => finiteMoment κ W n j) atTop (𝓝 (moment κ W n))) :
    3 * moment κ W n / 4 < finiteMoment κ W n (batchLevel κ W n) := by
…
```
Mentions: OAI.SLEExactGauge.Target.WienerLaw, OAI.SLEExactGauge.Target.finiteMoment, OAI.SLEExactGauge.Target.moment, OAI.SLEExactGauge.Target.batchLevel
theorem OAI.SLEExactGauge.Target.batchLevel_retains_moment line 65