Continuity and smoothness of the angular mean

The angular mean 𝒫u = (2π)⁻¹ ∫₀^{2π} ℛ_φ u dφ of eq:interior:average is as regular as u on the unit cylinder: if u is continuous (respectively C^n) on Q then so is 𝒫u. This is differentiation under the integral sign for a parametric integral over the compact angle interval [0, 2π], whose integrand (φ, z) ↦ Q_φ u(Q_φ⁻¹ x, t) is jointly C^n on ℝ × Q because the rotations preserve Q. For a C¹ field the spatial partial derivatives of the angular mean are the angular means of the spatial partial derivatives of the rotated fields (spatialPartial_angularMean).

The first section proves the general statement: an integral over Ioc a b of an integrand that is jointly C^n on ℝ × s, s open in a proper normed space, is C^n on s. The derivative under the integral sign is hasFDerivAt_integral_of_dominated_of_fderiv_le with the constant domination obtained from the compactness of [a, b] × closedBall x₀ ε; the induction on the order of differentiability follows contDiffOn_succ_iff_fderiv_of_isOpen.

Parametric integrals over a compact interval

theorem CIV.exists_closedBall_subset_bound_of_continuousOn {H : Type} [NormedAddCommGroup H] {s : Set H} {x₀ : H} [ProperSpace H] {E : Type} [NormedAddCommGroup E] (hs : IsOpen s) (hx₀ : x₀ ∈ s) {G : ℝ × H → E} (hG : ContinuousOn G (Set.univ ×ˢ s)) (a b : ℝ) : ∃ ε > 0, Metric.closedBall x₀ ε ⊆ s ∧ ∃ (M : ℝ), ∀ t ∈ Set.Icc a b, ∀ x ∈ Metric.closedBall x₀ ε, ‖G (t, x)‖ ≤ M

A function continuous on ℝ × s, s open, is bounded on [a, b] × closedBall x₀ ε for some closed ball inside s.

theorem CIV.continuous_section_of_continuousOn {H : Type} [NormedAddCommGroup H] {s : Set H} {E : Type} [TopologicalSpace E] {G : ℝ × H → E} (hG : ContinuousOn G (Set.univ ×ˢ s)) {x : H} (hx : x ∈ s) : Continuous fun (t : ℝ) => G (t, x)

The sections t ↦ G (t, x), x ∈ s, of a function continuous on ℝ × s.

theorem CIV.continuousAt_parametric_integral_Ioc {H : Type} [NormedAddCommGroup H] {s : Set H} {x₀ : H} [ProperSpace H] {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (hs : IsOpen s) (hx₀ : x₀ ∈ s) {G : ℝ × H → E} (hG : ContinuousOn G (Set.univ ×ˢ s)) (a b : ℝ) : ContinuousAt (fun (x : H) => ∫ (t : ℝ) in Set.Ioc a b, G (t, x)) x₀

Continuity of a parametric integral over Ioc a b with an integrand jointly continuous on ℝ × s.

theorem CIV.fderiv_section_of_contDiffOn {H : Type} [NormedAddCommGroup H] {s : Set H} [NormedSpace ℝ H] {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (hs : IsOpen s) {G : ℝ × H → E} (hG : ContDiffOn ℝ 1 G (Set.univ ×ˢ s)) (t : ℝ) {x : H} (hx : x ∈ s) : fderiv ℝ (fun (x : H) => G (t, x)) x = fderiv ℝ G (t, x) ∘SL ContinuousLinearMap.inr ℝ ℝ H

The partial derivative in the parameter of a function C¹ on ℝ × s, s open, is the composition of its derivative with the inclusion of the parameter factor.

theorem CIV.continuousOn_fderiv_section_of_contDiffOn {H : Type} [NormedAddCommGroup H] {s : Set H} [NormedSpace ℝ H] {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (hs : IsOpen s) {G : ℝ × H → E} (hG : ContDiffOn ℝ 1 G (Set.univ ×ˢ s)) : ContinuousOn (fun (p : ℝ × H) => fderiv ℝ (fun (x : H) => G (p.1, x)) p.2) (Set.univ ×ˢ s)

The partial derivative in the parameter of a function C¹ on ℝ × s, s open, is jointly continuous there.

theorem CIV.hasFDerivAt_parametric_integral_Ioc {H : Type} [NormedAddCommGroup H] {s : Set H} {x₀ : H} [NormedSpace ℝ H] [ProperSpace H] {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (hs : IsOpen s) (hx₀ : x₀ ∈ s) {G : ℝ × H → E} (hG : ContDiffOn ℝ 1 G (Set.univ ×ˢ s)) (a b : ℝ) : HasFDerivAt (fun (x : H) => ∫ (t : ℝ) in Set.Ioc a b, G (t, x)) (∫ (t : ℝ) in Set.Ioc a b, fderiv ℝ (fun (x : H) => G (t, x)) x₀) x₀

Differentiation under the integral sign for a parametric integral over Ioc a b with an integrand that is C¹ on ℝ × s: the derivative is the integral of the partial derivative in the parameter.

theorem CIV.contDiffOn_parametric_integral_Ioc_nat {H : Type} [NormedAddCommGroup H] {s : Set H} [NormedSpace ℝ H] [ProperSpace H] (hs : IsOpen s) (a b : ℝ) (n : ℕ) {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] {G : ℝ × H → E} : ContDiffOn ℝ (↑n) G (Set.univ ×ˢ s) → ContDiffOn ℝ (↑n) (fun (x : H) => ∫ (t : ℝ) in Set.Ioc a b, G (t, x)) s

A parametric integral over Ioc a b with an integrand jointly C^n on ℝ × s, n : ℕ, is C^n on s.

theorem CIV.contDiffOn_parametric_integral_Ioc {H : Type} [NormedAddCommGroup H] {s : Set H} [NormedSpace ℝ H] [ProperSpace H] {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (hs : IsOpen s) (a b : ℝ) (n : ℕ∞) {G : ℝ × H → E} (hG : ContDiffOn ℝ (↑n) G (Set.univ ×ˢ s)) : ContDiffOn ℝ (↑n) (fun (x : H) => ∫ (t : ℝ) in Set.Ioc a b, G (t, x)) s

A parametric integral over Ioc a b with an integrand jointly C^n on ℝ × s is C^n on s.

theorem CIV.contDiffOn_parametric_intervalIntegral {H : Type} [NormedAddCommGroup H] {s : Set H} [NormedSpace ℝ H] [ProperSpace H] {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] (hs : IsOpen s) {a b : ℝ} (hab : a ≤ b) (n : ℕ∞) {G : ℝ × H → E} (hG : ContDiffOn ℝ (↑n) G (Set.univ ×ˢ s)) : ContDiffOn ℝ (↑n) (fun (x : H) => ∫ (t : ℝ) in a..b, G (t, x)) s

A parametric interval integral x ↦ ∫ t in a..b, G (t, x), a ≤ b, with an integrand jointly C^n on ℝ × s is C^n on s.

The rotated field is jointly smooth

theorem CIV.isOpen_unitCylinder_prod : IsOpen unitCylinder

The unit cylinder is open for the product topology of Vec3 × ℝ.

theorem CIV.contDiff_rotZ_uncurry (n : WithTop ℕ∞) : ContDiff ℝ n fun (p : ℝ × CKN.Foundation.Parabolic.Vec3) => rotZ p.1 p.2

Joint smoothness of the rotation in the angle and the point.

theorem CIV.contDiffOn_rotField_uncurry (n : WithTop ℕ∞) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ n (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) : ContDiffOn ℝ n (fun (p : ℝ × CKN.Foundation.Parabolic.Vec3 × ℝ) => rotField p.1 u p.2) (Set.univ ×ˢ unitCylinder)

The rotated field (φ, z) ↦ (ℛ_φ u)(z) is jointly C^n on ℝ × Q when u is C^n on Q.

Regularity of the angular mean

theorem CIV.contDiffOn_angularMean (n : ℕ∞) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑n) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) : ContDiffOn ℝ (↑n) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => angularMean u z) unitCylinder

The angular mean of a C^n field on the unit cylinder is C^n there.

theorem CIV.contDiffOn_angularMean_smooth {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => angularMean u z) unitCylinder

The angular mean of a smooth field on the unit cylinder is smooth there.

theorem CIV.continuousOn_angularMean {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) : ContinuousOn (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => angularMean u z) unitCylinder

The angular mean of a continuous field on the unit cylinder is continuous there.

theorem CIV.spatialPartial_angularMean (i j : Fin 3) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ 1 (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => angularMean u w i) j z = (2 * Real.pi)⁻¹ * ∫ (φ : ℝ) in 0..2 * Real.pi, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => rotField φ u w i) j z

For a C¹ field, a spatial partial derivative of the angular mean is the angular mean of the corresponding spatial partial derivatives of the rotated fields: the derivative passes under the angular integral.