SourcePlaneIntegral.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The original measurable source integrand passes from separately chosen line predictors to the plane. No joint measurability of those auxiliary predictors is required, and no global integrability of the integrand is assumed. The final scale dependence is exactly the top area.

theorem OAI.LipschitzHilbert.source_plane_integral_of_tiled_lines line 15

theorem OAI.LipschitzHilbert.source_plane_area_bound line 36

Source documentation

The actual top-weight integral contributes precisely K² times its area and a fixed profile integral depending only on D.

theorem source_plane_area_bound (T : SlopeBox) {K D : ℝ}
    (hK : 0 < K) (hD : 2 < D) (s H C : ℝ) (hH : 0 < H)
    (f : ℝ × ℝ → ℝ) (hfmeas : AEStronglyMeasurable f (volume.prod volume))
    (hf : ∀ z, 0 ≤ f z)
    (hlocal : ∀ᵐ y : ℝ ∂volume, ∀ k : ℤ,
      IntegrableOn (fun x => f (x,y+s*x)) (sourceLineTile H k) volume ∧
      (∫ x in sourceLineTile H k, f (x,y+s*x)) ≤
        C*∫ x in sourceLineTile H k, T.weight K D (x,y+s*x)) :
    Integrable f (volume.prod volume) ∧
      (∫ z, f z ∂volume.prod volume) ≤
        (C*(2^D*∫ z, topProfile D z ∂volume.prod volume))*K^2*T.length*T.width := by
…

Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.sourceLineTile, OAI.LipschitzHilbert.topProfile

theorem OAI.LipschitzHilbert.source_plane_finite_area_sum line 55

Source documentation

Finite top sums retain the same area constant. All original integrands are integrable before their integrals are interchanged.

theorem source_plane_finite_area_sum {ι : Type*} (tops : Finset ι) (T : ι → SlopeBox)
    {K D : ℝ} (hK : 0 < K) (hD : 2 < D) (s H : ι → ℝ) (hH : ∀ i ∈ tops, 0 < H i)
    (C : ℝ) (f : ι → ℝ × ℝ → ℝ)
    (hfmeas : ∀ i ∈ tops, AEStronglyMeasurable (f i) (volume.prod volume))
    (hf : ∀ i ∈ tops, ∀ z, 0 ≤ f i z)
    (hlocal : ∀ i ∈ tops, ∀ᵐ y : ℝ ∂volume, ∀ k : ℤ,
      IntegrableOn (fun x => f i (x,y+s i*x)) (sourceLineTile (H i) k) volume ∧
      (∫ x in sourceLineTile (H i) k, f i (x,y+s i*x)) ≤
        C*∫ x in sourceLineTile (H i) k, (T i).weight K D (x,y+s i*x)) :
    Integrable (fun z => ∑ i ∈ tops, f i z) (volume.prod volume) ∧
      (∫ z, ∑ i ∈ tops, f i z ∂volume.prod volume) ≤
        ((C*(2^D*∫ z, topProfile D z ∂volume.prod volume))*K^2)*
…

Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.sourceLineTile, OAI.LipschitzHilbert.topProfile