Integration and averages on parabolic cylinders

Adapted from PDEFoundation (EllipticRegularity, 2026) with the author's permission. This independent module records generic average identities and the product-measure formulas used on balls and parabolic cylinders.

The source-facing scale-invariant quantities are intentionally not defined here.

Measures and cylinder Fubini

theorem CKN.Foundation.Parabolic.Integration.volume_parabolicPoint_eq_prod : MeasureTheory.volume = MeasureTheory.volume.prod MeasureTheory.volume

The volume measure on ParabolicPoint is the product of spatial and time volume.

theorem CKN.Foundation.Parabolic.Integration.volume_vec3Ball_pos {x : Vec3} {r : ℝ} (hr : 0 < r) : 0 < MeasureTheory.volume (vec3Ball x r)

A positive-radius Euclidean spatial ball has positive volume.

theorem CKN.Foundation.Parabolic.Integration.volume_vec3Ball_lt_top {x : Vec3} {r : ℝ} : MeasureTheory.volume (vec3Ball x r) < ⊤

A Euclidean spatial ball has finite volume.

theorem CKN.Foundation.Parabolic.Integration.volume_parabolicCylinder_pos {x : Vec3} {t r : ℝ} (hr : 0 < r) : 0 < MeasureTheory.volume (parabolicCylinder x t r)

A positive-radius parabolic cylinder has positive volume.

theorem CKN.Foundation.Parabolic.Integration.volume_parabolicCylinder_lt_top {x : Vec3} {t r : ℝ} : MeasureTheory.volume (parabolicCylinder x t r) < ⊤

A parabolic cylinder has finite volume.

theorem CKN.Foundation.Parabolic.Integration.integral_parabolicCylinder {x : Vec3} {t r : ℝ} {g : ParabolicPoint → ℝ} (hg : MeasureTheory.IntegrableOn g (parabolicCylinder x t r) MeasureTheory.volume) : ∫ (z : ParabolicPoint) in parabolicCylinder x t r, g z = ∫ (s : ℝ) in Set.Ioc (t - r ^ 2) t, ∫ (y : Vec3) in vec3Ball x r, g (y, s)

Fubini's theorem on a parabolic cylinder for Bochner-integrable functions.

theorem CKN.Foundation.Parabolic.Integration.lintegral_parabolicCylinder {x : Vec3} {t r : ℝ} {g : ParabolicPoint → ENNReal} (hg : AEMeasurable g (MeasureTheory.volume.restrict (parabolicCylinder x t r))) : ∫⁻ (z : ParabolicPoint) in parabolicCylinder x t r, g z = ∫⁻ (s : ℝ) in Set.Ioc (t - r ^ 2) t, ∫⁻ (y : Vec3) in vec3Ball x r, g (y, s)

Tonelli's theorem on a parabolic cylinder for nonnegative extended-real functions.

Generic averages

theorem CKN.Foundation.Parabolic.Integration.setAverage_eq_toReal_inv_smul {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : MeasureTheory.Measure α) (s : Set α) (f : α → E) : ⨍ (x : α) in s, f x ∂μ = (μ s).toReal⁻¹ • ∫ (x : α) in s, f x ∂μ

The set average is the integral against the reciprocal real measure.

theorem CKN.Foundation.Parabolic.Integration.setAverage_add_of_integrableOn {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ℝ} (hf : MeasureTheory.IntegrableOn f s μ) (hg : MeasureTheory.IntegrableOn g s μ) : ⨍ (x : α) in s, (f + g) x ∂μ = ⨍ (x : α) in s, f x ∂μ + ⨍ (x : α) in s, g x ∂μ

Set averages are additive when both summands are integrable.

theorem CKN.Foundation.Parabolic.Integration.setAverage_sub_of_integrableOn {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ℝ} (hf : MeasureTheory.IntegrableOn f s μ) (hg : MeasureTheory.IntegrableOn g s μ) : ⨍ (x : α) in s, (f - g) x ∂μ = ⨍ (x : α) in s, f x ∂μ - ⨍ (x : α) in s, g x ∂μ

Set averages commute with subtraction under integrability.

theorem CKN.Foundation.Parabolic.Integration.setAverage_const_of_pos_of_lt_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hsPos : 0 < μ s) (hsTop : μ s < ⊤) (c : ℝ) : ⨍ (_x : α) in s, c ∂μ = c

The average of a constant on a positive finite-measure set is that constant.

theorem CKN.Foundation.Parabolic.Integration.setAverage_nonneg_of_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ℝ} (hf : 0 ≤ᵐ[μ.restrict s] f) : 0 ≤ ⨍ (x : α) in s, f x ∂μ

Set averages preserve nonnegativity almost everywhere.

theorem CKN.Foundation.Parabolic.Integration.setAverage_norm_le {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : MeasureTheory.Measure α) (s : Set α) (f : α → E) : ‖⨍ (x : α) in s, f x ∂μ‖ ≤ ⨍ (x : α) in s, ‖f x‖ ∂μ

The norm of an average is bounded by the average of the norm.

theorem CKN.Foundation.Parabolic.Integration.setAverage_mono_of_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ℝ} (hf : MeasureTheory.IntegrableOn f s μ) (hg : MeasureTheory.IntegrableOn g s μ) (hfg : f ≤ᵐ[μ.restrict s] g) : ⨍ (x : α) in s, f x ∂μ ≤ ⨍ (x : α) in s, g x ∂μ

Set averages are monotone almost everywhere.