Splitting the two-reflection energy integral #
This module isolates the ENNReal integral algebra from concrete energy
densities. The resulting theorem is applied only after the density has been
made opaque at the use site.
theorem
CKN.lintegral_reflection_split_coeff
{A : Set (Vec 3)}
:
MeasurableSet A →
∀ (a b : ENNReal) (g : Vec 3 → ENNReal) (hg : Measurable g),
∫⁻ (y : Vec 3) in A, a * g (seeleyReflectionOne y) + b * g (seeleyReflectionTwo y) = (a * ∫⁻ (y : Vec 3) in A, g (seeleyReflectionOne y)) + b * ∫⁻ (y : Vec 3) in A, g (seeleyReflectionTwo y)
theorem
CKN.lintegral_reflection_split
{A : Set (Vec 3)}
(hA : MeasurableSet A)
(g : Vec 3 → ENNReal)
(hg : Measurable g)
: