Rotations about the vertical axis and the angular mean

Basic properties of the rotation rotZ, the rotated field rotField, and the angular mean angularMean of eq:interior:average: the group law of the rotations, their 2π-periodicity, preservation of the Euclidean norm and hence of the balls centred on the axis and of the unit cylinder, linearity and smoothness in the space variable, the rotation invariance of the angular mean, and the equivalence of IsAxisymmetricOn with pointwise rotation invariance on a rotation-invariant set (Section sec:aniso:notation).

None of the statements needs an integrability hypothesis: the change of variables in the angular integral is the translation invariance of the interval integral of a periodic function, and the rotation commutes with the integral because it is a continuous linear automorphism.

Components and the group law

@[simp]

theorem CIV.rotZ_apply_zero (φ : ℝ) (x : CKN.Foundation.Parabolic.Vec3) : rotZ φ x 0 = Real.cos φ * x 0 - Real.sin φ * x 1

@[simp]

theorem CIV.rotZ_apply_one (φ : ℝ) (x : CKN.Foundation.Parabolic.Vec3) : rotZ φ x 1 = Real.sin φ * x 0 + Real.cos φ * x 1

@[simp]

theorem CIV.rotZ_apply_two (φ : ℝ) (x : CKN.Foundation.Parabolic.Vec3) : rotZ φ x 2 = x 2

A rotation about the vertical axis does not move the vertical coordinate.

theorem CIV.rotZ_zero_apply (x : CKN.Foundation.Parabolic.Vec3) : rotZ 0 x = x

theorem CIV.rotZ_zero : rotZ 0 = id

theorem CIV.rotZ_add (φ ψ : ℝ) (x : CKN.Foundation.Parabolic.Vec3) : rotZ (φ + ψ) x = rotZ φ (rotZ ψ x)

The group law Q_{φ+ψ} = Q_φ Q_ψ.

theorem CIV.rotZ_neg_rotZ (φ : ℝ) (x : CKN.Foundation.Parabolic.Vec3) : rotZ (-φ) (rotZ φ x) = x

theorem CIV.rotZ_rotZ_neg (φ : ℝ) (x : CKN.Foundation.Parabolic.Vec3) : rotZ φ (rotZ (-φ) x) = x

theorem CIV.rotZ_injective (φ : ℝ) : Function.Injective (rotZ φ)

theorem CIV.rotZ_surjective (φ : ℝ) : Function.Surjective (rotZ φ)

theorem CIV.rotZ_periodic : Function.Periodic rotZ (2 * Real.pi)

The rotations are 2π-periodic in the angle.

theorem CIV.rotZ_add_two_pi (φ : ℝ) : rotZ (φ + 2 * Real.pi) = rotZ φ

theorem CIV.rotZ_sub_two_pi (φ : ℝ) : rotZ (φ - 2 * Real.pi) = rotZ φ

Linearity, continuity, and smoothness in the space variable

theorem CIV.rotZ_add_vec (φ : ℝ) (x y : CKN.Foundation.Parabolic.Vec3) : rotZ φ (x + y) = rotZ φ x + rotZ φ y

theorem CIV.rotZ_smul (φ c : ℝ) (x : CKN.Foundation.Parabolic.Vec3) : rotZ φ (c • x) = c • rotZ φ x

theorem CIV.rotZ_zero_vec (φ : ℝ) : rotZ φ 0 = 0

theorem CIV.rotZ_neg_vec (φ : ℝ) (x : CKN.Foundation.Parabolic.Vec3) : rotZ φ (-x) = -rotZ φ x

theorem CIV.rotZ_sub_vec (φ : ℝ) (x y : CKN.Foundation.Parabolic.Vec3) : rotZ φ (x - y) = rotZ φ x - rotZ φ y

theorem CIV.continuous_rotZ (φ : ℝ) : Continuous (rotZ φ)

theorem CIV.continuous_rotZ_uncurry : Continuous fun (p : ℝ × CKN.Foundation.Parabolic.Vec3) => rotZ p.1 p.2

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

noncomputable def CIV.rotZEquiv (φ : ℝ) : CKN.Foundation.Parabolic.Vec3 ≃L[ℝ] CKN.Foundation.Parabolic.Vec3

The rotation rotZ φ as a continuous linear automorphism of Vec3, with inverse rotZ (-φ).

Equations

• CIV.rotZEquiv φ = { toFun := CIV.rotZ φ, map_add' := ⋯, map_smul' := ⋯, invFun := CIV.rotZ (-φ), left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem CIV.rotZEquiv_apply (φ : ℝ) (x : CKN.Foundation.Parabolic.Vec3) : (rotZEquiv φ) x = rotZ φ x

@[simp]

theorem CIV.rotZEquiv_symm_apply (φ : ℝ) (x : CKN.Foundation.Parabolic.Vec3) : (rotZEquiv φ).symm x = rotZ (-φ) x

theorem CIV.contDiff_rotZ (φ : ℝ) (n : WithTop ℕ∞) : ContDiff ℝ n (rotZ φ)

theorem CIV.contDiff_rotZ_smooth (φ : ℝ) : ContDiff ℝ (↑⊤) (rotZ φ)

The axis and the meridional plane

theorem CIV.rotZ_meridional (φ x₁ x₃ : ℝ) : rotZ φ (meridional x₁ x₃) = ![Real.cos φ * x₁, Real.sin φ * x₁, x₃]

The rotation of a point of the meridional plane {x₂ = 0}.

theorem CIV.rotZ_axis (φ z : ℝ) : rotZ φ ![0, 0, z] = ![0, 0, z]

Every rotation fixes the vertical axis pointwise.

The Euclidean norm, balls centred on the axis, and the unit cylinder

theorem CIV.vec3EuclideanNorm_rotZ (φ : ℝ) (x : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.vec3EuclideanNorm (rotZ φ x) = CKN.Foundation.Parabolic.vec3EuclideanNorm x

Rotations preserve the Euclidean norm.

theorem CIV.rotZ_mem_vec3Ball_zero_iff (φ r : ℝ) (x : CKN.Foundation.Parabolic.Vec3) : rotZ φ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 r ↔ x ∈ CKN.Foundation.Parabolic.vec3Ball 0 r

theorem CIV.rotZ_mem_unitCylinder_iff (φ : ℝ) (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) : (rotZ φ x, t) ∈ unitCylinder ↔ (x, t) ∈ unitCylinder

theorem CIV.rotZ_mem_unitCylinder (φ : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ unitCylinder) : (rotZ φ z.1, z.2) ∈ unitCylinder

The unit cylinder is invariant under every rotation about the axis.

The rotated field

theorem CIV.rotField_apply (φ : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : rotField φ u z = rotZ φ (u (rotZ (-φ) z.1, z.2))

theorem CIV.rotField_zero (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : rotField 0 u = u

theorem CIV.rotField_rotField (φ ψ : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : rotField φ (rotField ψ u) = rotField (φ + ψ) u

The rotated fields compose according to the group law, ℛ_φ ℛ_ψ = ℛ_{φ+ψ}.

theorem CIV.rotField_neg_rotField (φ : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : rotField (-φ) (rotField φ u) = u

theorem CIV.rotField_rotField_neg (φ : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : rotField φ (rotField (-φ) u) = u

theorem CIV.rotField_add_two_pi (φ : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : rotField (φ + 2 * Real.pi) u = rotField φ u

theorem CIV.rotField_periodic (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : Function.Periodic (fun (φ : ℝ) => rotField φ u z) (2 * Real.pi)

At a fixed point, the rotated field is a 2π-periodic function of the angle.

The angular mean

theorem CIV.angularMean_apply (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : angularMean u z = (2 * Real.pi)⁻¹ • ∫ (φ : ℝ) in 0..2 * Real.pi, rotField φ u z

theorem CIV.intervalIntegral_comp_add_left_of_periodic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : ℝ → E} {T : ℝ} (hF : Function.Periodic F T) (ψ : ℝ) : ∫ (φ : ℝ) in 0..T, F (ψ + φ) = ∫ (φ : ℝ) in 0..T, F φ

The integral over a period of a periodic function is translation invariant.

theorem CIV.rotZ_intervalIntegral (ψ : ℝ) (F : ℝ → CKN.Foundation.Parabolic.Vec3) (a b : ℝ) : rotZ ψ (∫ (φ : ℝ) in a..b, F φ) = ∫ (φ : ℝ) in a..b, rotZ ψ (F φ)

A rotation commutes with the interval integral of a vector field.

theorem CIV.isAxisymmetricOn_of_forall_rotField_eq {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {S : Set CKN.Foundation.Parabolic.ParabolicPoint} (h : ∀ (φ : ℝ), ∀ z ∈ S, rotField φ u z = u z) : IsAxisymmetricOn u S

A field fixed by every rotation is its own angular mean.

theorem CIV.angularMean_eq_of_forall_rotField_eq {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (h : ∀ (φ : ℝ), rotField φ u = u) : angularMean u = u

theorem CIV.rotField_angularMean (ψ : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : rotField ψ (angularMean u) = angularMean u

The angular mean is fixed by every rotation: ℛ_ψ 𝒫u = 𝒫u.

theorem CIV.angularMean_rotField (ψ : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : angularMean (rotField ψ u) = angularMean u

The angular mean of a rotated field is the angular mean of the field: 𝒫 ℛ_ψ u = 𝒫u.

theorem CIV.angularMean_angularMean (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : angularMean (angularMean u) = angularMean u

The angular mean is a projection: 𝒫 𝒫u = 𝒫u.

theorem CIV.isAxisymmetricOn_angularMean (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (S : Set CKN.Foundation.Parabolic.ParabolicPoint) : IsAxisymmetricOn (angularMean u) S

Axisymmetry on a set

theorem CIV.IsAxisymmetricOn.mono {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {S T : Set CKN.Foundation.Parabolic.ParabolicPoint} (h : IsAxisymmetricOn u T) (hST : S ⊆ T) : IsAxisymmetricOn u S

theorem CIV.isAxisymmetricOn_univ_iff (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : IsAxisymmetricOn u Set.univ ↔ angularMean u = u

theorem CIV.IsAxisymmetricOn.rotField_eq {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {S : Set CKN.Foundation.Parabolic.ParabolicPoint} (h : IsAxisymmetricOn u S) (hS : ∀ (φ : ℝ), ∀ z ∈ S, (rotZ φ z.1, z.2) ∈ S) (φ : ℝ) {z : CKN.Foundation.Parabolic.ParabolicPoint} (hz : z ∈ S) : rotField φ u z = u z

On a rotation-invariant set, an axisymmetric field is fixed pointwise by every rotation.

theorem CIV.isAxisymmetricOn_iff {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {S : Set CKN.Foundation.Parabolic.ParabolicPoint} (hS : ∀ (φ : ℝ), ∀ z ∈ S, (rotZ φ z.1, z.2) ∈ S) : IsAxisymmetricOn u S ↔ ∀ (φ : ℝ), ∀ z ∈ S, rotField φ u z = u z

On a rotation-invariant set, axisymmetry is pointwise invariance under every rotation.

theorem CIV.isAxisymmetricOn_unitCylinder_iff (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : IsAxisymmetricOn u unitCylinder ↔ ∀ (φ : ℝ), ∀ z ∈ unitCylinder, rotField φ u z = u z

Axisymmetry on the unit cylinder is pointwise rotation invariance there.