SourceSelectorPlaneIntegral.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Original-selector marked bounds pass from each terminal line window to the plane. The measurable integrand is the original active path; the locally chosen marked factors need no joint measurability.

theorem OAI.LipschitzHilbert.source_path_integral_transfer_on line 17

Source documentation

A measurable nonnegative integrand can be dominated only on the integration set. No comparison outside that set is needed.

theorem source_path_integral_transfer_on {X : Type*} [MeasurableSpace X]
    (μ : Measure X) (s good : Set X) (hs : MeasurableSet s)
    (w active marked : X → ℝ) (C P : ℝ) (hC : 0 ≤ C)
    (hw : ∀ x, 0 ≤ w x) (ha : ∀ x ∈ good, 0 ≤ active x)
    (hmeas : AEStronglyMeasurable (good.indicator (fun x => w x*active x)) (μ.restrict s))
    (hint : IntegrableOn (good.indicator (fun x => w x*marked x)) s μ)
    (hbound : (∫ x in s, good.indicator (fun y => w y*marked y) x ∂μ) ≤
      P*(∫ x in s, w x ∂μ))
    (hpath : ∀ x ∈ s, x ∈ good → active x ≤ C*marked x) :
    IntegrableOn (good.indicator (fun x => w x*active x)) s μ ∧
      (∫ x in s, good.indicator (fun y => w y*active y) x ∂μ) ≤
        (C*P)*(∫ x in s, w x ∂μ) := by
…

theorem OAI.LipschitzHilbert.AngularGrid.eventually_source_selector_plane_integral line 56