Set integration as a bounded functional on L², and its commutation with Bochner averages.

noncomputable def EulerSetIntegralL2.setIntegralL2 {X : Type u_1} {V : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] (s : Set X) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) : ↥(MeasureTheory.Lp V 2 μ) →L[ℝ] V

Integration on a finite-measure set as a genuine bounded linear map on L².

Equations

• EulerSetIntegralL2.setIntegralL2 s hs hμs = (ContinuousLinearMap.lpPairing μ 2 2 (ContinuousLinearMap.lsmul ℝ ℝ)) (MeasureTheory.indicatorConstLp 2 hs hμs 1)

theorem EulerSetIntegralL2.setIntegralL2_apply {X : Type u_1} {V : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] (s : Set X) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (f : ↥(MeasureTheory.Lp V 2 μ)) : (setIntegralL2 s hs hμs) f = ∫ (x : X) in s, ↑↑f x ∂μ

theorem EulerSetIntegralL2.setIntegral_integral_L2 {X : Type u_1} {V : Type u_2} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] {Y : Type u_3} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} (s : Set X) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (F : Y → ↥(MeasureTheory.Lp V 2 μ)) (hF : MeasureTheory.Integrable F ν) : ∫ (x : X) in s, ↑↑(∫ (y : Y), F y ∂ν) x ∂μ = ∫ (y : Y), ∫ (x : X) in s, ↑↑(F y) x ∂μ ∂ν

Bochner averaging of L² elements commutes with integration on every finite-measure set.

theorem EulerSetIntegralL2.euclideanCover_neg (period : ℝ) (y : EulerSobolev.Domain 4) : EulerCylinderCoordinates.euclideanCover period (-y) = -EulerCylinderCoordinates.euclideanCover period y

theorem EulerSetIntegralL2.mollify_setIntegral (period : ℝ) [Fact (0 < period)] (n : ℕ) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) (s : Set (EulerLiftedGradientSpace.LiftDomain period)) (hs : MeasurableSet s) (hμs : (EulerLiftedGradientSpace.liftMeasure period) s ≠ ⊤) : ∫ (x : EulerLiftedGradientSpace.LiftDomain period) in s, ↑↑(EulerCylinderMollifier.mollify period n f) x ∂EulerLiftedGradientSpace.liftMeasure period = ∫ (y : EulerSobolev.Domain 4), ∫ (x : EulerLiftedGradientSpace.LiftDomain period) in s, EulerCylinderMollifier.mollifierKernel n y • ↑↑f (x - EulerCylinderCoordinates.euclideanCover period y) ∂EulerLiftedGradientSpace.liftMeasure period

The Bochner L² mollifier and the classical convolution have the same iterated finite-set integrals.