Joint reflection for arbitrary Hilbert-valued cylinder fields and their actual supported spaces.

noncomputable def EulerCylinderFieldReflection.reflection (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] : ↥(EulerLpCylinderTranslation.CylinderL2 P V) →ₗᵢ[ℝ] ↥(EulerLpCylinderTranslation.CylinderL2 P V)

Reflection, given by Lp.compMeasurePreservingₗᵢ ℝ (fun x : LiftDomain P => -x) (EulerCylinderReflection.measurePreserving_reflection P).

Equations

• EulerCylinderFieldReflection.reflection P = MeasureTheory.Lp.compMeasurePreservingₗᵢ ℝ (fun (x : EulerLiftedGradientSpace.LiftDomain P) => -x) ⋯

theorem EulerCylinderFieldReflection.reflection_ae (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : ↥(EulerLpCylinderTranslation.CylinderL2 P V)) : ↑↑((reflection P) u) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] fun (x : EulerLiftedGradientSpace.LiftDomain P) => ↑↑u (-x)

theorem EulerCylinderFieldReflection.reflection_involutive (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : ↥(EulerLpCylinderTranslation.CylinderL2 P V)) : (reflection P) ((reflection P) u) = u

theorem EulerCylinderFieldReflection.reflection_of_representative (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : ↥(EulerLpCylinderTranslation.CylinderL2 P V)) (f : EulerLiftedGradientSpace.LiftDomain P → V) (hf : ↑↑u =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) (c : ℝ) (hc : ∀ (x : EulerLiftedGradientSpace.LiftDomain P), f (-x) = c • f x) : (reflection P) u = c • u

theorem EulerCylinderFieldReflection.representative_of_reflection (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (u : ↥(EulerLpCylinderTranslation.CylinderL2 P V)) (f : EulerLiftedGradientSpace.LiftDomain P → V) (hf : ↑↑u =ᵐ[EulerLiftedGradientSpace.liftMeasure P] f) (hcont : Continuous f) (c : ℝ) (hc : (reflection P) u = c • u) (x : EulerLiftedGradientSpace.LiftDomain P) : f (-x) = c • f x

noncomputable def EulerCylinderFieldReflection.pathReflection (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Type u_2} [TopologicalSpace K] : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P V)) →L[ℝ] C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P V))

Path reflection, given by (reflection P).toContinuousLinearMap.compLeftContinuous ℝ K.

Equations

• EulerCylinderFieldReflection.pathReflection P = ContinuousLinearMap.compLeftContinuous ℝ K (EulerCylinderFieldReflection.reflection P).toContinuousLinearMap

@[simp]

theorem EulerCylinderFieldReflection.pathReflection_apply (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {K : Type u_2} [TopologicalSpace K] (u : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P V))) (t : K) : ((pathReflection P) u) t = (reflection P) (u t)

theorem EulerCylinderFieldReflection.reflection_fullOperator (P : ℝ) [Fact (0 < P)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (A : BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F)) (hA : ∀ (x : EulerSmoothLimit.Space), A (-x) = A x) (u : ↥(EulerLpCylinderTranslation.CylinderL2 P E)) : (reflection P) (((EulerLpCylinderRectangular.fullOperatorMap P) A) u) = ((EulerLpCylinderRectangular.fullOperatorMap P) A) ((reflection P) u)

theorem EulerCylinderFieldReflection.reflection_mem (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ S ↔ x ∈ S) (u : ↥(EulerLpCylinderPaths.Supported P V S hS)) : (reflection P) ↑u ∈ EulerLpCylinderPaths.Supported P V S hS

noncomputable def EulerCylinderFieldReflection.supportedReflection (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ S ↔ x ∈ S) : ↥(EulerLpCylinderPaths.Supported P V S hS) →L[ℝ] ↥(EulerLpCylinderPaths.Supported P V S hS)

Supported reflection as an element of Supported P V S hS →L[ℝ] Supported P V S hS.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem EulerCylinderFieldReflection.supportedReflection_coe (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ S ↔ x ∈ S) (u : ↥(EulerLpCylinderPaths.Supported P V S hS)) : ↑((supportedReflection P S hS hSym) u) = (reflection P) ↑u

noncomputable def EulerCylinderFieldReflection.supportedPathReflection (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ S ↔ x ∈ S) {K : Type u_2} [TopologicalSpace K] : C(K, ↥(EulerLpCylinderPaths.Supported P V S hS)) →L[ℝ] C(K, ↥(EulerLpCylinderPaths.Supported P V S hS))

Supported path reflection, given by (supportedReflection P S hS hSym).compLeftContinuous ℝ K.

Equations

• EulerCylinderFieldReflection.supportedPathReflection P S hS hSym = ContinuousLinearMap.compLeftContinuous ℝ K (EulerCylinderFieldReflection.supportedReflection P S hS hSym)

@[simp]

theorem EulerCylinderFieldReflection.supportedPathReflection_apply (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ S ↔ x ∈ S) {K : Type u_2} [TopologicalSpace K] (u : C(K, ↥(EulerLpCylinderPaths.Supported P V S hS))) (t : K) : ((supportedPathReflection P S hS hSym) u) t = (supportedReflection P S hS hSym) (u t)

theorem EulerCylinderFieldReflection.supportedReflection_operator (P : ℝ) [Fact (0 < P)] {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] (S : Set EulerSmoothLimit.Space) (hS : MeasurableSet S) (hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ S ↔ x ∈ S) (A : BoundedContinuousFunction EulerSmoothLimit.Space (E →L[ℝ] F)) (hA : ∀ (x : EulerSmoothLimit.Space), A (-x) = A x) (u : ↥(EulerLpCylinderPaths.Supported P E S hS)) : (supportedReflection P S hS hSym) (((EulerLpCylinderRectangular.supportedOperatorMap P S hS) A) u) = ((EulerLpCylinderRectangular.supportedOperatorMap P S hS) A) ((supportedReflection P S hS hSym) u)