TiledPredictionIntegral.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Cellwise constructed predictions give the reference-line and planar integral bounds. Auxiliary choices need no joint measurability.

structure OAI.LipschitzHilbert.LineCellMajorant line 19
Source documentation
The finite prediction data on one actual line mesh.
```
structure LineCellMajorant (g : FiniteLineGrid) (T : SlopeBox)
    (K D y B : ℝ) (f : ℝ → ℝ) where
…
```
Mentions: OAI.LipschitzHilbert.FiniteLineGrid, OAI.LipschitzHilbert.SlopeBox
theorem OAI.LipschitzHilbert.LineCellMajorant.integral_bound line 31
theorem OAI.LipschitzHilbert.tiled_prediction_integral line 58

theorem OAI.LipschitzHilbert.planar_prediction_integral line 78

Source documentation

Only the original integrand is required to be planar measurable. All snapshot choices may be made separately on almost every reference line.

theorem planar_prediction_integral (T : SlopeBox) (origin H : ℝ) (hH : 0 < H)
    (G N : ℕ) (hG : 0 < G) {K D B : ℝ}
    (hK : 1 ≤ K) (hD : 2 < D) (hB : 0 ≤ B) (hwidth : H ≤ T.length)
    (f : ℝ × ℝ → ℝ) (hf : AEStronglyMeasurable f (volume.prod volume))
    (hf0 : ∀ z, 0 ≤ f z)
    (hp : ∀ᵐ y ∂volume, ∀ k : ℤ, Nonempty (LineCellMajorant
      (tiledLineGrid origin H hH G N hG k) T K D y B
      (fun x => f (x, y + T.slope * x)))) :
    Integrable f (volume.prod volume) ∧
      (∫ z, f z ∂volume.prod volume) ≤
        B * Real.exp (2 * D) * ∫ z, T.weight K D z ∂volume.prod volume := by
…

Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.LineCellMajorant, OAI.LipschitzHilbert.tiledLineGrid