Odd parity of the actual common correction and pressure assembled from finite genuine solutions.

Reflection invariance of the concrete lifted-gradient space and pressure solve.

theorem EulerGradientReflection.reflection_testGradient (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (φ : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hφ : HasCompactSupport φ ∧ ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerLiftedGradientSpace.localLift period φ x)) : (EulerCylinderReflection.reflection period) (EulerLiftedGradientSpace.testGradientLp period κ m φ hφ) = -EulerLiftedGradientSpace.testGradientLp period κ m (EulerCylinderReflection.reflectedTest period φ) ⋯

Reflecting a genuine smooth test gradient gives the negative gradient of the reflected scalar test.

theorem EulerGradientReflection.gradientSpace_reflection_mem (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) {g : ↥(EulerLiftedGradientSpace.LiftL2 period)} (hg : g ∈ EulerLiftedGradientSpace.gradientSpace period κ m) : (EulerCylinderReflection.reflection period) g ∈ EulerLiftedGradientSpace.gradientSpace period κ m

Reflection preserves the closure of the span of actual test gradients.

theorem EulerGradientReflection.gradientSpace_map_reflection (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) : Submodule.map (EulerCylinderReflection.reflection period).toLinearMap (EulerLiftedGradientSpace.gradientSpace period κ m) = EulerLiftedGradientSpace.gradientSpace period κ m

Reflection maps the concrete lifted-gradient subspace onto itself.

theorem EulerGradientReflection.gradientProjection_reflection (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (EulerCylinderReflection.reflection period) ((EulerLiftedGradientSpace.gradientProjection period κ m) f) = (EulerLiftedGradientSpace.gradientProjection period κ m) ((EulerCylinderReflection.reflection period) f)

The genuine orthogonal gradient projection commutes with joint reflection.

theorem EulerGradientReflection.divergenceFreeSpace_reflection_mem (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) {f : ↥(EulerLiftedGradientSpace.LiftL2 period)} (hf : f ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) : (EulerCylinderReflection.reflection period) f ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m

The actual weak divergence-free constraint is preserved by reflection.

theorem EulerGradientReflection.coefficientOperator_reflection (period : ℝ) [Fact (0 < period)] (A : EulerSpatialSobolevInverse.SmoothCoefficient period) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), A.coefficient (-x) = A.coefficient x) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (EulerCylinderReflection.reflection period) (A.operator f) = A.operator ((EulerCylinderReflection.reflection period) f)

An even coefficient field commutes with the actual reflection isometry.

theorem EulerGradientReflection.pressure_reflection (period : ℝ) [Fact (0 < period)] (A : EulerSpatialSobolevInverse.SmoothCoefficient period) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), A.coefficient (-x) = A.coefficient x) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (EulerCylinderReflection.reflection period) (A.pressure κ m c hc hpos f) = A.pressure κ m c hc hpos ((EulerCylinderReflection.reflection period) f)

Uniqueness of the concrete coercive pressure inverse proves its reflection covariance for the actual even metric.

Joint reflection on the actual complete cylinder Sobolev spaces.

noncomputable def EulerSobolevReflection.reflectionArrayOperator (period : ℝ) [Fact (0 < period)] (q : ℕ) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] EulerCylinderSobolevSpace.SobolevWord q → ↥(EulerLiftedGradientSpace.LiftL2 period)

Reflection of a derivative array includes the sign of each derivative word.

Equations

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

theorem EulerSobolevReflection.reflectionArray_mem (period : ℝ) [Fact (0 < period)] (q : ℕ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (reflectionArrayOperator period q) u ∈ ↑(EulerCylinderSobolevSpace.sobolevSubspace period q)

The signed derivative array satisfies the actual strong-derivative compatibility.

noncomputable def EulerSobolevReflection.sobolevReflection (period : ℝ) [Fact (0 < period)] (q : ℕ) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

Joint pullback reflection as a genuine bounded map of the complete Sobolev space.

Equations

• EulerSobolevReflection.sobolevReflection period q = (EulerSobolevReflection.reflectionArrayOperator period q).codRestrict ↑(EulerCylinderSobolevSpace.sobolevSubspace period q) ⋯

@[simp]

theorem EulerSobolevReflection.sobolevReflection_apply (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (w : EulerCylinderSobolevSpace.SobolevWord q) : ↑((sobolevReflection period q) u) w = (-1) ^ ↑w.fst • (EulerCylinderReflection.reflection period) (↑u w)

The derivative coordinates of reflection have exactly the alternating signs.

@[simp]

theorem EulerSobolevReflection.value_sobolevReflection (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : EulerCylinderSobolevSpace.value period ((sobolevReflection period q) u) = (EulerCylinderReflection.reflection period) (EulerCylinderSobolevSpace.value period u)

The underlying field is the actual L² pullback by joint negation.

@[simp]

theorem EulerSobolevReflection.sobolevReflection_involutive (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (sobolevReflection period q) ((sobolevReflection period q) u) = u

Joint reflection is involutive on the complete Sobolev space.

theorem EulerSobolevReflection.sobolevReflection_word_norm (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (w : EulerCylinderSobolevSpace.SobolevWord q) : ‖↑((sobolevReflection period q) u) w‖ = ‖↑u w‖

Every genuine derivative coordinate keeps its L² norm under reflection.

theorem EulerSobolevReflection.sobolevReflection_norm (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ‖(sobolevReflection period q) u‖ = ‖u‖

Reflection preserves the actual finite Sobolev norm.

theorem EulerSobolevReflection.sobolevReflection_sumNorm (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : EulerCylinderSobolevSpace.sumNorm period ((sobolevReflection period q) u) = EulerCylinderSobolevSpace.sumNorm period u

Reflection also preserves the source's sum-over-derivatives Sobolev norm.

theorem EulerSobolevReflection.truncate_reflection (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : (EulerCylinderSobolevSpace.truncateOperator period q) ((sobolevReflection period (q + 1)) u) = (sobolevReflection period q) ((EulerCylinderSobolevSpace.truncateOperator period q) u)

Truncating the Sobolev order commutes with actual reflection.

theorem EulerSobolevReflection.derivative_reflection (period : ℝ) [Fact (0 < period)] {q : ℕ} (i : Fin 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : (EulerCylinderSobolevSpace.derivativeOperator period q i) ((sobolevReflection period (q + 1)) u) = -(sobolevReflection period q) ((EulerCylinderSobolevSpace.derivativeOperator period q i) u)

Every actual coordinate derivative reverses sign under joint reflection.

noncomputable def EulerSobolevReflection.oddReflection (period : ℝ) [Fact (0 < period)] (q : ℕ) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The symmetry whose fixed points are odd velocity fields.

Equations

• EulerSobolevReflection.oddReflection period q = -EulerSobolevReflection.sobolevReflection period q

@[simp]

theorem EulerSobolevReflection.oddReflection_apply (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (oddReflection period q) u = -(sobolevReflection period q) u

Odd reflection is represented by minus the field at the reflected point.

theorem EulerSobolevReflection.oddReflection_involutive (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (oddReflection period q) ((oddReflection period q) u) = u

The signed reflection is involutive.

theorem EulerSobolevReflection.oddReflection_norm (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ‖(oddReflection period q) u‖ = ‖u‖

The signed reflection preserves the Sobolev norm.

theorem EulerSobolevReflection.oddReflection_divergenceFree (period : ℝ) [Fact (0 < period)] {q : ℕ} (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hu : EulerCylinderSobolevSpace.value period u ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m) : EulerCylinderSobolevSpace.value period ((oddReflection period q) u) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m

Signed reflection preserves the genuine weak divergence constraint.

Joint odd symmetry of the actual correction source and its coercive pressure.

Reflection covariance of the literal Sobolev product, transport and pressure operators.

@[instance_reducible]

noncomputable def EulerSobolevParityOperators.paritySobolevGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The inherited Sobolev additive normed-group instance.

Equations

• EulerSobolevParityOperators.paritySobolevGroup period q = inferInstance

@[instance_reducible]

noncomputable def EulerSobolevParityOperators.paritySobolevSpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The inherited real Sobolev module instance.

Equations

• EulerSobolevParityOperators.paritySobolevSpace period q = inferInstance

@[instance_reducible]

noncomputable def EulerSobolevParityOperators.parityBilinearGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : SeminormedAddCommGroup (↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period q))

The inherited normed-group instance on the actual bilinear operator space.

Equations

• EulerSobolevParityOperators.parityBilinearGroup period q = inferInstance

theorem EulerSobolevParityOperators.product_reflection (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (EulerSobolevReflection.sobolevReflection period q) (EulerSobolevL2Product.productHq period hq L hL u v) = EulerSobolevL2Product.productHq period hq L hL ((EulerSobolevReflection.sobolevReflection period q) u) ((EulerSobolevReflection.sobolevReflection period q) v)

Reflection of the actual Sobolev product is the product of reflected fields.

theorem EulerSobolevParityOperators.product_neg_right (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : EulerSobolevL2Product.productHq period hq L hL u (-v) = -EulerSobolevL2Product.productHq period hq L hL u v

The actual bilinear Sobolev product changes sign in its second input.

theorem EulerSobolevParityOperators.transport_reflection (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : ((EulerSobolevTransport.transportBilinear period hq L hL) ((EulerSobolevReflection.sobolevReflection period (q + 1)) u)) ((EulerSobolevReflection.sobolevReflection period (q + 1)) v) = -(EulerSobolevReflection.sobolevReflection period q) (((EulerSobolevTransport.transportBilinear period hq L hL) u) v)

The literal transport operator reverses under joint pullback reflection.

theorem EulerSobolevParityOperators.coefficient_reflection (period : ℝ) [Fact (0 < period)] {q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q A) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), A.coefficient (-x) = A.coefficient x) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (EulerSobolevReflection.sobolevReflection period q) ((EulerSobolevCoefficientPressure.coefficientSobolevOperator period K) u) = (EulerSobolevCoefficientPressure.coefficientSobolevOperator period K) ((EulerSobolevReflection.sobolevReflection period q) u)

Actual even coefficient multiplication commutes with Sobolev reflection.

theorem EulerSobolevParityOperators.odd_coefficient_L2_reflection (period : ℝ) [Fact (0 < period)] (A : EulerSpatialSobolevInverse.SmoothCoefficient period) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), A.coefficient (-x) = -A.coefficient x) (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : (EulerCylinderReflection.reflection period) (A.operator f) = -A.operator ((EulerCylinderReflection.reflection period) f)

Actual odd coefficient multiplication anticommutes with the L² reflection.

theorem EulerSobolevParityOperators.odd_coefficient_reflection (period : ℝ) [Fact (0 < period)] {q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q A) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), A.coefficient (-x) = -A.coefficient x) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (EulerSobolevReflection.sobolevReflection period q) ((EulerSobolevCoefficientPressure.coefficientSobolevOperator period K) u) = -(EulerSobolevCoefficientPressure.coefficientSobolevOperator period K) ((EulerSobolevReflection.sobolevReflection period q) u)

Actual odd coefficient multiplication anticommutes with Sobolev reflection.

theorem EulerSobolevParityOperators.pressureSobolev_reflection (period : ℝ) [Fact (0 < period)] {q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q A) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), A.coefficient (-x) = A.coefficient x) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (EulerSobolevReflection.sobolevReflection period q) ((EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos) u) = (EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos) ((EulerSobolevReflection.sobolevReflection period q) u)

The concrete coercive pressure acts covariantly at every Sobolev order.

theorem EulerSobolevParityOperators.projectedSource_reflection (period : ℝ) [Fact (0 < period)] {q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q A) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), A.coefficient (-x) = A.coefficient x) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (EulerSobolevReflection.sobolevReflection period q) ((EulerSobolevCoefficientPressure.projectedSourceOperator period K κ m c hc hpos) u) = (EulerSobolevCoefficientPressure.projectedSourceOperator period K κ m c hc hpos) ((EulerSobolevReflection.sobolevReflection period q) u)

The actual pressure-corrected forcing commutes with reflection for an even metric.

theorem EulerSobolevParityOperators.coordinateProduct_reflection (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (i : Fin 3) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : ((EulerCorrectionOperators.coordinateProduct period hq i) ((EulerSobolevReflection.sobolevReflection period (q + 1)) u)) ((EulerSobolevReflection.sobolevReflection period (q + 1)) v) = (EulerSobolevReflection.sobolevReflection period q) (((EulerCorrectionOperators.coordinateProduct period hq i) u) v)

The coordinate product reflects without a derivative sign.

theorem EulerSobolevParityOperators.algebraic_reflection (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (A : Fin 3 → EulerSpatialSobolevInverse.SmoothCoefficient period) (K : (i : Fin 3) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (A i)) (hA : ∀ (i : Fin 3) (x : EulerLiftedGradientSpace.LiftDomain period), (A i).coefficient (-x) = -(A i).coefficient x) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : ((EulerCorrectionOperators.algebraicBilinear period hq fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K i)) ((EulerSobolevReflection.sobolevReflection period (q + 1)) u)) ((EulerSobolevReflection.sobolevReflection period (q + 1)) v) = -(EulerSobolevReflection.sobolevReflection period q) (((EulerCorrectionOperators.algebraicBilinear period hq fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K i)) u) v)

The actual algebraic Euler term reverses reflection because its coefficient fields, κ F⁻¹ ∂ᵢF, are odd.

theorem EulerSobolevParityOperators.eulerBilinear_reflection (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (A : Fin 3 → EulerSpatialSobolevInverse.SmoothCoefficient period) (K : (i : Fin 3) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (A i)) (hA : ∀ (i : Fin 3) (x : EulerLiftedGradientSpace.LiftDomain period), (A i).coefficient (-x) = -(A i).coefficient x) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : ((EulerCorrectionOperators.eulerBilinear period hq L hL fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K i)) ((EulerSobolevReflection.sobolevReflection period (q + 1)) u)) ((EulerSobolevReflection.sobolevReflection period (q + 1)) v) = -(EulerSobolevReflection.sobolevReflection period q) (((EulerCorrectionOperators.eulerBilinear period hq L hL fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K i)) u) v)

The literal Euler bilinear term reverses pullback reflection.

theorem EulerSobolevParityOperators.eulerBilinear_oddReflection (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (A : Fin 3 → EulerSpatialSobolevInverse.SmoothCoefficient period) (K : (i : Fin 3) → EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q (A i)) (hA : ∀ (i : Fin 3) (x : EulerLiftedGradientSpace.LiftDomain period), (A i).coefficient (-x) = -(A i).coefficient x) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : (EulerSobolevReflection.oddReflection period q) (((EulerCorrectionOperators.eulerBilinear period hq L hL fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K i)) u) v) = ((EulerCorrectionOperators.eulerBilinear period hq L hL fun (i : Fin 3) => EulerSobolevCoefficientPressure.coefficientSobolevOperator period (K i)) ((EulerSobolevReflection.oddReflection period (q + 1)) u)) ((EulerSobolevReflection.oddReflection period (q + 1)) v)

Signed reflection is an exact symmetry of the actual bilinear Euler term.

theorem EulerCorrectionParity.linearized_source_equivariant {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (R : X →L[ℝ] X) (S : Y →L[ℝ] Y) (B : X →L[ℝ] X →L[ℝ] Y) (C : X →L[ℝ] Y) (z : X) (r : Y) (hB : ∀ (u v : X), S ((B u) v) = (B (R u)) (R v)) (hC : ∀ (u : X), S (C u) = C (R u)) (hz : R z = z) (hr : S r = r) (e : X) : S (r + (EulerCorrectionOperators.linearize B C z) e + (B e) e) = r + (EulerCorrectionOperators.linearize B C z) (R e) + (B (R e)) (R e)

Exact equivariance of the residual plus the linearized quadratic increment.

@[instance_reducible]

noncomputable def EulerCorrectionParity.correctionParityGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The inherited Sobolev additive normed-group instance.

Equations

• EulerCorrectionParity.correctionParityGroup period q = inferInstance

@[instance_reducible]

noncomputable def EulerCorrectionParity.correctionParitySpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The inherited real Sobolev module instance.

Equations

• EulerCorrectionParity.correctionParitySpace period q = inferInstance

theorem EulerCorrectionParity.value_oddReflection (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : EulerCylinderSobolevSpace.value period ((EulerSobolevReflection.oddReflection period q) u) = -(EulerCylinderReflection.reflection period) (EulerCylinderSobolevSpace.value period u)

Signed reflection on Sobolev fields has the literal signed L² value.

theorem EulerCorrectionParity.oddReflection_fixed_of_ae (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hu : ∀ᵐ (x : EulerLiftedGradientSpace.LiftDomain period) ∂EulerLiftedGradientSpace.liftMeasure period, ↑↑(EulerCylinderSobolevSpace.value period u) (-x) = -↑↑(EulerCylinderSobolevSpace.value period u) x) : (EulerSobolevReflection.oddReflection period q) u = u

Actual almost-everywhere odd parity is precisely a fixed point of signed reflection.

theorem EulerCorrectionParity.truncate_oddReflection (period : ℝ) [Fact (0 < period)] {q : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : (EulerCylinderSobolevSpace.truncateOperator period q) ((EulerSobolevReflection.oddReflection period (q + 1)) u) = (EulerSobolevReflection.oddReflection period q) ((EulerCylinderSobolevSpace.truncateOperator period q) u)

Signed reflection commutes with restriction to the next Sobolev order.

theorem EulerCorrectionParity.coefficient_oddReflection (period : ℝ) [Fact (0 < period)] {q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q A) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), A.coefficient (-x) = A.coefficient x) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (EulerSobolevReflection.oddReflection period q) ((EulerSobolevCoefficientPressure.coefficientSobolevOperator period K) u) = (EulerSobolevCoefficientPressure.coefficientSobolevOperator period K) ((EulerSobolevReflection.oddReflection period q) u)

An actual even coefficient commutes with signed reflection.

theorem EulerCorrectionParity.pressure_oddReflection (period : ℝ) [Fact (0 < period)] {q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q A) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), A.coefficient (-x) = A.coefficient x) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (EulerSobolevReflection.oddReflection period q) ((EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos) u) = (EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos) ((EulerSobolevReflection.oddReflection period q) u)

The actual pressure inverse commutes with signed reflection for an even metric.

theorem EulerCorrectionParity.projectedSource_oddReflection (period : ℝ) [Fact (0 < period)] {q : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection q A) (hA : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), A.coefficient (-x) = A.coefficient x) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (EulerSobolevReflection.oddReflection period q) ((EulerSobolevCoefficientPressure.projectedSourceOperator period K κ m c hc hpos) u) = (EulerSobolevCoefficientPressure.projectedSourceOperator period K κ m c hc hpos) ((EulerSobolevReflection.oddReflection period q) u)

The actual pressure-corrected source commutes with signed reflection.

theorem EulerCorrectionParity.rawSource_oddReflection (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) {T : Type u_3} [TopologicalSpace T] (D : EulerCorrectionOperators.CorrectionData period q T) (t : T) (hL : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), (D.linear.coefficient t).coefficient (-x) = (D.linear.coefficient t).coefficient x) (hQ : ∀ (i : Fin 3) (x : EulerLiftedGradientSpace.LiftDomain period), ((D.quadratic i).coefficient t).coefficient (-x) = -((D.quadratic i).coefficient t).coefficient x) (hz : (EulerSobolevReflection.oddReflection period (q + 1)) (D.approximation t) = D.approximation t) (hr : (EulerSobolevReflection.oddReflection period q) (D.residual t) = D.residual t) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : (EulerSobolevReflection.oddReflection period q) (EulerCorrectionOperators.CorrectionData.rawSource period D hq t e) = EulerCorrectionOperators.CorrectionData.rawSource period D hq t ((EulerSobolevReflection.oddReflection period (q + 1)) e)

The literal non-pressure correction source has odd-reflection symmetry under the source's actual even linear and odd quadratic coefficients.

theorem EulerCorrectionParity.correction_pressure_oddReflection (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) {T : Type u_3} [TopologicalSpace T] (D : EulerCorrectionOperators.CorrectionData period q T) (t : T) (hG : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), (D.metric.coefficient t).coefficient (-x) = (D.metric.coefficient t).coefficient x) (hL : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), (D.linear.coefficient t).coefficient (-x) = (D.linear.coefficient t).coefficient x) (hQ : ∀ (i : Fin 3) (x : EulerLiftedGradientSpace.LiftDomain period), ((D.quadratic i).coefficient t).coefficient (-x) = -((D.quadratic i).coefficient t).coefficient x) (hz : (EulerSobolevReflection.oddReflection period (q + 1)) (D.approximation t) = D.approximation t) (hr : (EulerSobolevReflection.oddReflection period q) (D.residual t) = D.residual t) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : (EulerSobolevReflection.oddReflection period q) (EulerCorrectionOperators.CorrectionData.pressure period D hq t e) = EulerCorrectionOperators.CorrectionData.pressure period D hq t ((EulerSobolevReflection.oddReflection period (q + 1)) e)

The genuine correction pressure transforms by signed reflection, with its sign fixed by the actual pressure definition.

theorem EulerCorrectionParity.correction_source_oddReflection (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) {T : Type u_3} [TopologicalSpace T] (D : EulerCorrectionOperators.CorrectionData period q T) (t : T) (hG : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), (D.metric.coefficient t).coefficient (-x) = (D.metric.coefficient t).coefficient x) (hL : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), (D.linear.coefficient t).coefficient (-x) = (D.linear.coefficient t).coefficient x) (hQ : ∀ (i : Fin 3) (x : EulerLiftedGradientSpace.LiftDomain period), ((D.quadratic i).coefficient t).coefficient (-x) = -((D.quadratic i).coefficient t).coefficient x) (hz : (EulerSobolevReflection.oddReflection period (q + 1)) (D.approximation t) = D.approximation t) (hr : (EulerSobolevReflection.oddReflection period q) (D.residual t) = D.residual t) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : (EulerSobolevReflection.oddReflection period q) ((EulerCorrectionOperators.CorrectionData.coefficients period D hq).apply t e) = (EulerCorrectionOperators.CorrectionData.coefficients period D hq).apply t ((EulerSobolevReflection.oddReflection period (q + 1)) e)

The literal projected nonlinear correction equation has the required odd symmetry, derived from the concrete parity of its prescribed fields.

Odd parity of actual inviscid correction solutions, proved by genuine PDE uniqueness.

@[instance_reducible]

noncomputable def EulerInviscidCorrectionParity.inviscidParityGroup (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedAddCommGroup ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The inherited finite Sobolev normed-group instance.

Equations

• EulerInviscidCorrectionParity.inviscidParityGroup period q = inferInstance

@[instance_reducible]

noncomputable def EulerInviscidCorrectionParity.inviscidParitySpace (period : ℝ) [Fact (0 < period)] (q : ℕ) : NormedSpace ℝ ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The inherited real finite Sobolev module instance.

Equations

• EulerInviscidCorrectionParity.inviscidParitySpace period q = inferInstance

theorem EulerInviscidCorrectionParity.inviscid_correction_odd (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) (T : ℝ) (hT : 0 ≤ T) (D : EulerCorrectionOperators.CorrectionData period q ↑(Set.Icc 0 T)) (B : EulerCorrectionStabilityBudget.StabilityBudget period hT D) (hG : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period), (D.metric.coefficient t).coefficient (-x) = (D.metric.coefficient t).coefficient x) (hL : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period), (D.linear.coefficient t).coefficient (-x) = (D.linear.coefficient t).coefficient x) (hQ : ∀ (t : ↑(Set.Icc 0 T)) (i : Fin 3) (x : EulerLiftedGradientSpace.LiftDomain period), ((D.quadratic i).coefficient t).coefficient (-x) = -((D.quadratic i).coefficient t).coefficient x) (hzOdd : ∀ (t : ↑(Set.Icc 0 T)), (EulerSobolevReflection.oddReflection period (q + 1)) (D.approximation t) = D.approximation t) (hrOdd : ∀ (t : ↑(Set.Icc 0 T)), (EulerSobolevReflection.oddReflection period q) (D.residual t) = D.residual t) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hi : u ⟨0, ⋯⟩ = 0) (hu : ∀ (t : ℝ) (ht : t ∈ Set.Ioo 0 T), HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (EulerVolterraConvolution.extendPath T hT u r)) (EulerCylinderSobolevSpace.value period ((EulerCorrectionOperators.CorrectionData.coefficients period D hq).apply ⟨t, ⋯⟩ (u ⟨t, ⋯⟩))) t) (hz : ∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (D.approximation t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) (hud : ∀ (t : ↑(Set.Icc 0 T)), EulerCylinderSobolevSpace.value period (u t) ∈ EulerLiftedGradientSpace.divergenceFreeSpace period D.κ D.direction) (t : ↑(Set.Icc 0 T)) : (EulerSobolevReflection.oddReflection period (q + 1)) (u t) = u t

Every actual zero-initial inviscid correction is odd under the source's genuine parity hypotheses on the prescribed fields and coefficients. The reflected path solves the literal same equation; uniqueness is proved by the existing metric-energy theorem, not assumed.

theorem EulerInviscidCorrectionParity.inviscid_correction_pressure_odd (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 6 ≤ q) {T : Type u_1} [TopologicalSpace T] (D : EulerCorrectionOperators.CorrectionData period q T) (t : T) (hG : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), (D.metric.coefficient t).coefficient (-x) = (D.metric.coefficient t).coefficient x) (hL : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), (D.linear.coefficient t).coefficient (-x) = (D.linear.coefficient t).coefficient x) (hQ : ∀ (i : Fin 3) (x : EulerLiftedGradientSpace.LiftDomain period), ((D.quadratic i).coefficient t).coefficient (-x) = -((D.quadratic i).coefficient t).coefficient x) (hz : (EulerSobolevReflection.oddReflection period (q + 1)) (D.approximation t) = D.approximation t) (hr : (EulerSobolevReflection.oddReflection period q) (D.residual t) = D.residual t) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (hu : (EulerSobolevReflection.oddReflection period (q + 1)) u = u) : (EulerSobolevReflection.oddReflection period q) (EulerCorrectionOperators.CorrectionData.pressure period D hq t u) = EulerCorrectionOperators.CorrectionData.pressure period D hq t u

The actual signed coercive correction pressure has odd gradient parity at every time once the correction parity has been established.

Genuine continuous Sobolev realizations of the assembled correction and its actual pressure at every order.

noncomputable def EulerCorrectionAssembly.FiniteFamily.fieldTower (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) : EulerAllOrderCorrectionData.FieldTower period T

The assembled correction as one actual L² field with continuous Sobolev realizations at every order.

Equations

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

noncomputable def EulerCorrectionAssembly.FiniteFamily.pressureTower (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) : EulerAllOrderCorrectionData.FieldTower period T

The actual signed pressure as one L² field with continuous Sobolev realizations at every order.

Equations

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

theorem EulerCorrectionAssembly.FiniteFamily.solution_eq_realization (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (q : ℕ) (hq : 6 ≤ q) : F.solution q hq = (fieldTower period F C).realization (q + 1)

Each finite solution is exactly the common tower's realization at that same Sobolev order.

theorem EulerCorrectionAssembly.FiniteFamily.signedPressurePath_eq_realization (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (q : ℕ) (hq : 6 ≤ q) : signedPressurePath period F q hq = (pressureTower period F C).realization q

Every finite signed pressure is exactly the common pressure tower's realization at that order.

structure EulerCorrectionAssembly.ParityData (period : ℝ) [Fact (0 < period)] {T : ℝ} (A : EulerAllOrderCorrectionData.Data period T) : Prop

The prescribed source's actual joint spatial-angular parities. The metric and linear coefficients are even, the quadratic coefficient is odd, and the approximate velocity and residual are odd as actual L² fields.

• metric (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : (A.metric.coefficient t).coefficient (-x) = (A.metric.coefficient t).coefficient x

  The actual pressure metric is even.

• linear (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : (A.linear.coefficient t).coefficient (-x) = (A.linear.coefficient t).coefficient x

  The actual linear coefficient is even.

• quadratic (t : ↑(Set.Icc 0 T)) (i : Fin 3) (x : EulerLiftedGradientSpace.LiftDomain period) : ((A.quadratic i).coefficient t).coefficient (-x) = -((A.quadratic i).coefficient t).coefficient x

  Each actual quadratic coefficient is odd.

• approximation (t : ↑(Set.Icc 0 T)) : -(EulerCylinderReflection.reflection period) (A.approximation.field t) = A.approximation.field t

  The prescribed approximate velocity is an odd actual field.

• residual (t : ↑(Set.Icc 0 T)) : -(EulerCylinderReflection.reflection period) (A.residual.field t) = A.residual.field t

  The prescribed residual is an odd actual field.

theorem EulerCorrectionAssembly.fieldTower_realization_odd (period : ℝ) [Fact (0 < period)] {T : ℝ} (f : EulerAllOrderCorrectionData.FieldTower period T) (hf : ∀ (t : ↑(Set.Icc 0 T)), -(EulerCylinderReflection.reflection period) (f.field t) = f.field t) (q : ℕ) (t : ↑(Set.Icc 0 T)) : (EulerSobolevReflection.oddReflection period q) ((f.realization q) t) = (f.realization q) t

Oddness of the actual common L² field forces oddness of every Sobolev realization.

theorem EulerCorrectionAssembly.FiniteFamily.solution_odd (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (P : ParityData period A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : (EulerSobolevReflection.oddReflection period (q + 1)) ((F.solution q hq) t) = (F.solution q hq) t

Genuine PDE uniqueness makes every finite correction odd from the prescribed input parity.

theorem EulerCorrectionAssembly.FiniteFamily.commonPath_odd (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (P : ParityData period A) (t : ↑(Set.Icc 0 T)) : -(EulerCylinderReflection.reflection period) ((commonPath period F) t) = (commonPath period F) t

The actual assembled continuous L² correction is odd.

theorem EulerCorrectionAssembly.continuous_representative_odd (period : ℝ) [Fact (0 < period)] (u : ↥(EulerLiftedGradientSpace.LiftL2 period)) (g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : -(EulerCylinderReflection.reflection period) u = u) (hg : Continuous g) (hrep : ↑↑u =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (x : EulerLiftedGradientSpace.LiftDomain period) : g (-x) = -g x

A continuous representative of an actual odd L² field is pointwise odd.

theorem EulerCorrectionAssembly.FiniteFamily.pointField_odd (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (P : ParityData period A) (t : ↑(Set.Icc 0 T)) (x : EulerLiftedGradientSpace.LiftDomain period) : pointField period F t (-x) = -pointField period F t x

The canonical smooth correction is odd at every spatial and angular point.

theorem EulerCorrectionAssembly.FiniteFamily.signedPressurePath_odd (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (P : ParityData period A) (q : ℕ) (hq : 6 ≤ q) (t : ↑(Set.Icc 0 T)) : (EulerSobolevReflection.oddReflection period q) ((signedPressurePath period F q hq) t) = (signedPressurePath period F q hq) t

The actual signed coercive pressure is odd at every finite Sobolev order.

theorem EulerCorrectionAssembly.FiniteFamily.commonPressure_odd (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (P : ParityData period A) (t : ↑(Set.Icc 0 T)) : -(EulerCylinderReflection.reflection period) ((commonPressure period F) t) = (commonPressure period F) t

The actual assembled signed pressure gradient is odd in L².

theorem EulerCorrectionAssembly.FiniteFamily.fieldTower_odd (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (P : ParityData period A) (q : ℕ) (t : ↑(Set.Icc 0 T)) : (EulerSobolevReflection.oddReflection period q) (((fieldTower period F C).realization q) t) = ((fieldTower period F C).realization q) t

Every realization of the assembled correction tower is odd.

theorem EulerCorrectionAssembly.FiniteFamily.pressureTower_odd (period : ℝ) [Fact (0 < period)] {T : ℝ} {hT : 0 < T} {A : EulerAllOrderCorrectionData.Data period T} (F : FiniteFamily period hT A) (C : ComparisonData period hT A) (P : ParityData period A) (q : ℕ) (t : ↑(Set.Icc 0 T)) : (EulerSobolevReflection.oddReflection period q) (((pressureTower period F C).realization q) t) = ((pressureTower period F C).realization q) t

Every realization of the actual assembled signed pressure tower is odd.