Actual reflection symmetry of the mean packet solve

Even source matrices and an odd forcing commute through the complete mean form, including its localized initial boundary operator. The odd coordinate velocity follows from uniqueness of the constructed inverse.

Reflection covariance of the full mean variational inverse

Every identity concerns the real time derivative, terminal primitive, initial trace, and nonlocal boundary form. Uniqueness of the actual coercive inverse then transports reflection without an assumed symmetry of a solution.

Genuine spatial reflection on the mean time Hilbert spaces.

noncomputable def EulerMeanTimeReflection.solenoidalReflection : ↥EulerMeanSolenoidal.solenoidalSpace →ₗᵢ[ℝ] ↥EulerMeanSolenoidal.solenoidalSpace

Reflection restricted to the actual ordinary solenoidal subspace.

Equations

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

@[simp]

theorem EulerMeanTimeReflection.solenoidalReflection_coe (u : ↥EulerMeanSolenoidal.solenoidalSpace) : ↑(solenoidalReflection u) = EulerMeanSolenoidal.reflection ↑u

@[simp]

theorem EulerMeanTimeReflection.solenoidalReflection_involutive (u : ↥EulerMeanSolenoidal.solenoidalSpace) : solenoidalReflection (solenoidalReflection u) = u

noncomputable def EulerMeanTimeReflection.timeReflection (T : ℝ) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2) →ₗᵢ[ℝ] ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Time reflection, given by timeLiftIsometry T reflection.

Equations

• EulerMeanTimeReflection.timeReflection T = EulerTimeLpBoundedMap.timeLiftIsometry T EulerMeanSolenoidal.reflection

noncomputable def EulerMeanTimeReflection.timeSolenoidalReflection (T : ℝ) : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace) →ₗᵢ[ℝ] ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

Time solenoidal reflection, given by timeLiftIsometry T solenoidalReflection.

Equations

• EulerMeanTimeReflection.timeSolenoidalReflection T = EulerTimeLpBoundedMap.timeLiftIsometry T EulerMeanTimeReflection.solenoidalReflection

theorem EulerMeanTimeReflection.timeReflection_ae (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : ↑↑((timeReflection T) u) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => EulerMeanSolenoidal.reflection (↑↑u t)

theorem EulerMeanTimeReflection.timeSolenoidalReflection_ae (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : ↑↑((timeSolenoidalReflection T) u) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => solenoidalReflection (↑↑u t)

@[simp]

theorem EulerMeanTimeReflection.timeReflection_involutive (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : (timeReflection T) ((timeReflection T) u) = u

@[simp]

theorem EulerMeanTimeReflection.timeSolenoidalReflection_involutive (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (timeSolenoidalReflection T) ((timeSolenoidalReflection T) u) = u

theorem EulerMeanTimeReflection.timeReflection_inner_shift (T : ℝ) (u v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : inner ℝ ((timeReflection T) u) v = inner ℝ u ((timeReflection T) v)

theorem EulerMeanTimeReflection.timeSolenoidalReflection_inner_shift (T : ℝ) (u v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : inner ℝ ((timeSolenoidalReflection T) u) v = inner ℝ u ((timeSolenoidalReflection T) v)

theorem EulerMeanTimeReflection.timeReflection_realPrimitive (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) (t : ℝ) : EulerTerminalTimePrimitive.realPrimitive T ((timeReflection T) u) t = EulerMeanSolenoidal.reflection (EulerTerminalTimePrimitive.realPrimitive T u t)

theorem EulerMeanTimeReflection.timeSolenoidalReflection_realPrimitive (T : ℝ) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) (t : ℝ) : EulerTerminalTimePrimitive.realPrimitive T ((timeSolenoidalReflection T) u) t = solenoidalReflection (EulerTerminalTimePrimitive.realPrimitive T u t)

theorem EulerMeanTimeReflection.timeReflection_initialTrace (T : ℝ) (hT : 0 ≤ T) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : (EulerTerminalTimePrimitive.initialTrace T hT) ((timeReflection T) u) = EulerMeanSolenoidal.reflection ((EulerTerminalTimePrimitive.initialTrace T hT) u)

theorem EulerMeanTimeReflection.timeReflection_primitiveTimeLp (T : ℝ) (hT : 0 ≤ T) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : (EulerTerminalTimePrimitive.primitiveTimeLp T hT) ((timeReflection T) u) = (timeReflection T) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) u)

theorem EulerMeanTimeReflection.timeSolenoidalReflection_primitiveTimeLp (T : ℝ) (hT : 0 ≤ T) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (EulerTerminalTimePrimitive.primitiveTimeLp T hT) ((timeSolenoidalReflection T) u) = (timeSolenoidalReflection T) ((EulerTerminalTimePrimitive.primitiveTimeLp T hT) u)

@[instance_reducible]

noncomputable def EulerMeanFixedReflection.instMeanOperatorReflection1 : NormedAddCommGroup ↥EulerMeanSolenoidal.L2

Cache the standard NormedAddCommGroup L2 instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedReflection.instMeanOperatorReflection1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedReflection.instMeanOperatorReflection2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.L2

Cache the standard InnerProductSpace ℝ L2 instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedReflection.instMeanOperatorReflection2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedReflection.instMeanOperatorReflection3 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedReflection.instMeanOperatorReflection3 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedReflection.instMeanOperatorReflection4 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard InnerProductSpace ℝ solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedReflection.instMeanOperatorReflection4 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedReflection.instMeanOperatorReflection5 (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup (TimeLp T L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedReflection.instMeanOperatorReflection5 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedReflection.instMeanOperatorReflection6 (T : ℝ) : InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Cache the standard InnerProductSpace ℝ (TimeLp T L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedReflection.instMeanOperatorReflection6 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedReflection.instMeanOperatorReflection7 (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

Cache the standard NormedAddCommGroup (TimeLp T solenoidalSpace) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedReflection.instMeanOperatorReflection7 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedReflection.instMeanOperatorReflection8 (T : ℝ) : InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

Cache the standard InnerProductSpace ℝ (TimeLp T solenoidalSpace) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedReflection.instMeanOperatorReflection8 T = inferInstance

def EulerMeanFixedReflection.ReflectionInvariant (A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) : Prop

Reflection invariant, given by ∀ u, A (reflection u) = reflection (A u).

Equations

• EulerMeanFixedReflection.ReflectionInvariant A = ∀ (u : ↥EulerMeanSolenoidal.L2), A (EulerMeanSolenoidal.reflection u) = EulerMeanSolenoidal.reflection (A u)

theorem EulerMeanFixedReflection.timeMultiplier_reflection (T : ℝ) (hT : 0 ≤ T) (F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (hF : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (F t)) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : (EulerTimeLp.timeMultiplier T hT F) ((EulerMeanTimeReflection.timeReflection T) u) = (EulerMeanTimeReflection.timeReflection T) ((EulerTimeLp.timeMultiplier T hT F) u)

theorem EulerMeanFixedReflection.frameMultiplier_reflection (T : ℝ) (hT : 0 ≤ T) (F : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (hF : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (F t)) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (EulerTimeLp.timeMultiplier T hT (EulerMeanVariationalInverse.solenoidalFrame T F)) ((EulerMeanTimeReflection.timeSolenoidalReflection T) u) = (EulerMeanTimeReflection.timeReflection T) ((EulerTimeLp.timeMultiplier T hT (EulerMeanVariationalInverse.solenoidalFrame T F)) u)

Reflection covariance of the full mean variational inverse

Every identity concerns the real time derivative, terminal primitive, initial trace, and nonlocal boundary form. Uniqueness of the actual coercive inverse then transports reflection without an assumed symmetry of a solution.

@[instance_reducible]

noncomputable def EulerMeanFixedReflection.instMeanFixedReflection1 : NormedAddCommGroup ↥EulerMeanSolenoidal.L2

Cache the standard NormedAddCommGroup L2 instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedReflection.instMeanFixedReflection1 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedReflection.instMeanFixedReflection2 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.L2

Cache the standard InnerProductSpace ℝ L2 instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedReflection.instMeanFixedReflection2 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedReflection.instMeanFixedReflection3 : NormedAddCommGroup ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard NormedAddCommGroup solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedReflection.instMeanFixedReflection3 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedReflection.instMeanFixedReflection4 : InnerProductSpace ℝ ↥EulerMeanSolenoidal.solenoidalSpace

Cache the standard InnerProductSpace ℝ solenoidalSpace instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedReflection.instMeanFixedReflection4 = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedReflection.instMeanFixedReflection5 (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Cache the standard NormedAddCommGroup (TimeLp T L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedReflection.instMeanFixedReflection5 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedReflection.instMeanFixedReflection6 (T : ℝ) : InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)

Cache the standard InnerProductSpace ℝ (TimeLp T L2) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedReflection.instMeanFixedReflection6 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedReflection.instMeanFixedReflection7 (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

Cache the standard NormedAddCommGroup (TimeLp T solenoidalSpace) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedReflection.instMeanFixedReflection7 T = inferInstance

@[instance_reducible]

noncomputable def EulerMeanFixedReflection.instMeanFixedReflection8 (T : ℝ) : InnerProductSpace ℝ ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)

Cache the standard InnerProductSpace ℝ (TimeLp T solenoidalSpace) instance to shorten typeclass synthesis.

Equations

• EulerMeanFixedReflection.instMeanFixedReflection8 T = inferInstance

theorem EulerMeanFixedReflection.fixedMeanDerivative_reflection (T : ℝ) (hT : 0 ≤ T) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (hF : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (F t)) (hF₁ : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (F₁ t)) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (EulerMeanFixedSpaceInverse.fixedMeanDerivative T hT F F₁) ((EulerMeanTimeReflection.timeSolenoidalReflection T) u) = (EulerMeanTimeReflection.timeReflection T) ((EulerMeanFixedSpaceInverse.fixedMeanDerivative T hT F F₁) u)

theorem EulerMeanFixedReflection.fixedMeanPrimitive_reflection (T : ℝ) (hT : 0 ≤ T) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (hF : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (F t)) (hF₁ : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (F₁ t)) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (EulerMeanFixedSpaceInverse.fixedMeanPrimitive T hT F F₁) ((EulerMeanTimeReflection.timeSolenoidalReflection T) u) = (EulerMeanTimeReflection.timeReflection T) ((EulerMeanFixedSpaceInverse.fixedMeanPrimitive T hT F F₁) u)

theorem EulerMeanFixedReflection.fixedMeanTrace_reflection (T : ℝ) (hT : 0 ≤ T) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (hF : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (F t)) (hF₁ : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (F₁ t)) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (EulerMeanFixedSpaceInverse.fixedMeanTrace T hT F F₁) ((EulerMeanTimeReflection.timeSolenoidalReflection T) u) = EulerMeanSolenoidal.reflection ((EulerMeanFixedSpaceInverse.fixedMeanTrace T hT F F₁) u)

theorem EulerMeanFixedReflection.boundaryCoefficient_reflection (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (hM0 : ReflectionInvariant M0) (hA : ReflectionInvariant A) (u : ↥EulerMeanSolenoidal.L2) : (M0 + L • A) (EulerMeanSolenoidal.reflection u) = EulerMeanSolenoidal.reflection ((M0 + L • A) u)

theorem EulerMeanFixedReflection.fixedMeanForm_reflection (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (hF : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (F t)) (hF₁ : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (F₁ t)) (hH : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (H t)) (hM0 : ReflectionInvariant M0) (hA : ReflectionInvariant A) (u v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : inner ℝ ((EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) ((EulerMeanTimeReflection.timeSolenoidalReflection T) u)) ((EulerMeanTimeReflection.timeSolenoidalReflection T) v) = inner ℝ ((EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) u) v

theorem EulerMeanFixedReflection.eq_of_reflected_pairing (T : ℝ) (x y : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) (h : ∀ (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)), inner ℝ x ((EulerMeanTimeReflection.timeSolenoidalReflection T) v) = inner ℝ y ((EulerMeanTimeReflection.timeSolenoidalReflection T) v)) : x = y

theorem EulerMeanFixedReflection.fixedMeanOperator_reflection (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (hF : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (F t)) (hF₁ : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (F₁ t)) (hH : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (H t)) (hM0 : ReflectionInvariant M0) (hA : ReflectionInvariant A) (u : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)) : (EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) ((EulerMeanTimeReflection.timeSolenoidalReflection T) u) = (EulerMeanTimeReflection.timeSolenoidalReflection T) ((EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) u)

theorem EulerMeanFixedReflection.fixedMeanPrimitive_adjoint_reflection (T : ℝ) (hT : 0 ≤ T) (F F₁ : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (hF : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (F t)) (hF₁ : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (F₁ t)) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : (ContinuousLinearMap.adjoint (EulerMeanFixedSpaceInverse.fixedMeanPrimitive T hT F F₁)) ((EulerMeanTimeReflection.timeReflection T) f) = (EulerMeanTimeReflection.timeSolenoidalReflection T) ((ContinuousLinearMap.adjoint (EulerMeanFixedSpaceInverse.fixedMeanPrimitive T hT F F₁)) f)

theorem EulerMeanFixedReflection.coerciveSolution_reflection (T : ℝ) (hT : 0 ≤ T) (F F₁ H : C(↑(Set.Icc 0 T), ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2)) (M0 A : ↥EulerMeanSolenoidal.L2 →L[ℝ] ↥EulerMeanSolenoidal.L2) (L : ℝ) (hF : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (F t)) (hF₁ : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (F₁ t)) (hH : ∀ (t : ↑(Set.Icc 0 T)), ReflectionInvariant (H t)) (hM0 : ReflectionInvariant M0) (hA : ReflectionInvariant A) (c : ℝ) (hc : 0 < c) (hO : ∀ (v : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.solenoidalSpace)), c * ‖v‖ ^ 2 ≤ inner ℝ ((EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) v) v) (f : ↥(EulerTimeLp.TimeLp T ↥EulerMeanSolenoidal.L2)) : (EulerMeanTimeReflection.timeSolenoidalReflection T) ((EulerCoerciveProjection.coerciveInverse (EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) c hc hO) (-(ContinuousLinearMap.adjoint (EulerMeanFixedSpaceInverse.fixedMeanPrimitive T hT F F₁)) f)) = (EulerCoerciveProjection.coerciveInverse (EulerMeanFixedSpaceInverse.fixedMeanOperator T hT F F₁ H M0 A L) c hc hO) (-(ContinuousLinearMap.adjoint (EulerMeanFixedSpaceInverse.fixedMeanPrimitive T hT F F₁)) ((EulerMeanTimeReflection.timeReflection T) f))

Uniqueness of the actual coercive solve forces reflection covariance.

structure EulerMeanPacketProvider.EvenData (D : Data) : Prop

These are literal parity assumptions on the prescribed source coefficients.

• frame (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : (D.F.field t) (-x) = (D.F.field t) x
• frameDerivative (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : (D.F₁.field t) (-x) = (D.F₁.field t) x
• curvature (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : (D.H.field t) (-x) = (D.H.field t) x
• initialStrain (x : EulerSmoothLimit.Space) : D.M0.field (-x) = D.M0.field x
• strain (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : (D.M.field t) (-x) = (D.M.field t) x

theorem EulerMeanPacketProvider.multiplier_reflection_of_even (A : EulerMeanCoefficients.Field) (hA : ∀ (x : EulerSmoothLimit.Space), A (-x) = A x) : EulerMeanFixedReflection.ReflectionInvariant (EulerMeanCoefficients.multiplier A)

Actual pointwise multiplication by an even matrix field commutes with reflection.

noncomputable def EulerMeanPacketProvider.Data.coordinateSolver (D : Data) : ↥(EulerTimeLp.TimeLp D.T ↥EulerMeanSolenoidal.L2) →L[ℝ] ↥(EulerTimeLp.TimeLp D.T ↥EulerMeanSolenoidal.solenoidalSpace)

The actual source coordinate solve as a bounded linear operator.

Equations

• D.coordinateSolver = EulerMeanSourceFixedInverse.sourceCoordinateSolver D.T ⋯ D.ℓ ⋯ D.F D.F₁ D.H D.M0 D.opInv D.Be D.Bc D.L D.r ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ D.K ⋯ ⋯ ⋯ ⋯

theorem EulerMeanPacketProvider.Data.coordinateSolver_reflection (D : Data) (hD : EvenData D) (f : ↥(EulerTimeLp.TimeLp D.T ↥EulerMeanSolenoidal.L2)) : (EulerMeanTimeReflection.timeSolenoidalReflection D.T) (D.coordinateSolver f) = D.coordinateSolver ((EulerMeanTimeReflection.timeReflection D.T) f)

theorem EulerMeanPacketProvider.Forcing.velocityLp_eq_coordinateSolver {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) : G.solution.velocityLp = D.coordinateSolver G.lp

theorem EulerMeanPacketProvider.Forcing.path_reflection {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (hodd : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), raw (↑t, -x, 0) = -raw (↑t, x, 0)) (t : ↑(Set.Icc 0 D.T)) : EulerMeanSolenoidal.reflection (G.path t) = -G.path t

theorem EulerMeanPacketProvider.Forcing.lp_reflection {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (hodd : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), raw (↑t, -x, 0) = -raw (↑t, x, 0)) : (EulerMeanTimeReflection.timeReflection D.T) G.lp = -G.lp

theorem EulerMeanPacketProvider.Forcing.velocityLp_reflection {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (hodd : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), raw (↑t, -x, 0) = -raw (↑t, x, 0)) (hD : EvenData D) : (EulerMeanTimeReflection.timeSolenoidalReflection D.T) G.solution.velocityLp = -G.solution.velocityLp

theorem EulerMeanPacketProvider.Forcing.coordinate_velocity_reflection {D : Data} {raw : EulerPacketProfileRecursion.VectorField} (G : Forcing D raw) (hodd : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), raw (↑t, -x, 0) = -raw (↑t, x, 0)) (hD : EvenData D) (t : ↑(Set.Icc 0 D.T)) : EulerMeanTimeReflection.solenoidalReflection (G.solution.velocity ↑t) = -G.solution.velocity ↑t

Oddness of the actual L² solve holds pointwise for its continuous time representative.