Moduli and Lebesgue integrals of indicator truncations

The Marcinkiewicz interpolation argument used for the Caffarelli–Kohn–Nirenberg program (CKN 1982) splits a function into a high-frequency part, carried by a superlevel set of the ℝ≥0∞-valued modulus absE f x = ENNReal.ofReal |f x|, and a low-frequency part, carried by its complement. Both parts are indicator truncations s.indicator f of the original function.

This file records the three elementary identities needed for that bookkeeping. The first states that absE commutes with truncation pointwise, so that absE (s.indicator f) is the truncation of absE f and the modulus of a truncated function vanishes off s. The second and third state that the Lebesgue integrals of absE (s.indicator f) and of its square over all of Vec3 agree with the corresponding integrals over s alone. All three are stated for an arbitrary measurable set s and an arbitrary function f : Vec3 → ℝ; the two integral identities use the restriction of Lebesgue measure to s.

theorem CKN.Foundation.Euclidean.absE_indicator_eq (s : Set Parabolic.Vec3) (f : Parabolic.Vec3 → ℝ) : absE (s.indicator f) = s.indicator (absE f)

The ℝ≥0∞-valued modulus absE commutes with truncation by an indicator: truncating f to s before taking the modulus is the same as taking the modulus first and then truncating it to s.

theorem CKN.Foundation.Euclidean.lintegral_absE_indicator {s : Set Parabolic.Vec3} (hs : MeasurableSet s) (f : Parabolic.Vec3 → ℝ) : ∫⁻ (x : Parabolic.Vec3), absE (s.indicator f) x = ∫⁻ (x : Parabolic.Vec3) in s, absE f x

The total mass of the modulus of a truncation is the mass of the modulus over the truncating set: ∫ absE (s.indicator f) = ∫_s absE f.

theorem CKN.Foundation.Euclidean.lintegral_absE_indicator_sq {s : Set Parabolic.Vec3} (hs : MeasurableSet s) (f : Parabolic.Vec3 → ℝ) : ∫⁻ (x : Parabolic.Vec3), absE (s.indicator f) x ^ 2 = ∫⁻ (x : Parabolic.Vec3) in s, absE f x ^ 2

The same identity for the square of the modulus: ∫ absE (s.indicator f) ^ 2 = ∫_s absE f ^ 2.