Exact spatial differentiation of the actual nonlinear correction equation.

@[instance_reducible]

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

Cache the standard NormedAddCommGroup (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

• EulerGevreyDifferentiatedEquation.diffEqGroup period q = inferInstance

@[instance_reducible]

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

Cache the standard NormedSpace ℝ (SobolevSpace period q) instance to shorten typeclass synthesis.

Equations

• EulerGevreyDifferentiatedEquation.diffEqSpace period q = inferInstance

noncomputable def EulerGevreyDifferentiatedEquation.energyWordOperator (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (I : EulerGevreyMetricComparison.ExternalWord N) (a : EulerBaseWordMetric.BaseWord q) : ↥(EulerCylinderSobolevSpace.SobolevSpace period s) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

The actual continuous linear map taking one external and one base derivative word.

Equations

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

theorem EulerGevreyDifferentiatedEquation.energyWordOperator_apply (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (I : EulerGevreyMetricComparison.ExternalWord N) (a : EulerBaseWordMetric.BaseWord q) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : (energyWordOperator period q N hN I a) u = EulerGevreyMetricComparison.energyValues period q N hN u I a

This continuous operator is exactly the genuine jet word in the metric energy.

theorem EulerGevreyDifferentiatedEquation.energyValues_add (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerGevreyMetricComparison.energyValues period q N hN (u + v) = EulerGevreyMetricComparison.energyValues period q N hN u + EulerGevreyMetricComparison.energyValues period q N hN v

Genuine energy words are linear in the differentiated field.

theorem EulerGevreyDifferentiatedEquation.energyValues_sub (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerGevreyMetricComparison.energyValues period q N hN (u - v) = EulerGevreyMetricComparison.energyValues period q N hN u - EulerGevreyMetricComparison.energyValues period q N hN v

Genuine energy words commute with subtraction.

noncomputable def EulerGevreyDifferentiatedEquation.topTransport (period : ℝ) [Fact (0 < period)] {s : ℕ} (N : ℕ) (hN : N + 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : EulerGevreyMetricComparison.ExternalWord N → EulerBaseWordMetric.BaseWord 6 → ↥(EulerLiftedGradientSpace.LiftL2 period)

The literal undifferentiated transport acting on the final external/base derivative.

Equations

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

theorem EulerGevreyDifferentiatedEquation.transport_telescope (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (N : ℕ) (hN : N + 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : EulerGevreyForcingComponents.externalTransportForcing period hs N hN L hL u v + EulerGevreyBaseTransport.baseTransportForcing period N hN L hL u v = EulerGevreyMetricComparison.energyValues period 6 N hN (((EulerSobolevTransport.transportBilinear period hs L hL) u) v) - topTransport period N hN L u v

External and base transport commutators telescope to the exact differentiated transport.

theorem EulerGevreyDifferentiatedEquation.coefficient_word (period : ℝ) [Fact (0 < period)] {s n : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (p : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (hn : n ≤ s) (w : Fin n → Fin 4) : (EulerCylinderSobolevSpace.toJet period ((EulerSobolevCoefficientPressure.coefficientSobolevOperator period K) p)).word w = (EulerSpatialSobolevInverse.SpatialJet.multiply K (EulerCylinderSobolevSpace.toJet period p)).word w

Taking a word of the actual coefficient operator gives the word of its genuine product jet.

theorem EulerGevreyDifferentiatedEquation.externalPressure_as_difference (period : ℝ) [Fact (0 < period)] {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (K0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) (N : ℕ) (hN : N + 6 ≤ s) (p : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (I : EulerGevreyMetricComparison.ExternalWord N) (a : EulerBaseWordMetric.BaseWord 6) : EulerGevreyForcingComponents.externalPressureForcing period K N hN p I a = EulerCylinderSobolevSpace.value period ((EulerSobolevWordLevel.wordAtLevel period 0 (↑a.fst) a.snd ⋯) ((EulerSobolevWordLevel.wordAtLevel period 6 (↑I.fst) I.snd ⋯) ((EulerSobolevCoefficientPressure.coefficientSobolevOperator period K) p) - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period K0) ((EulerSobolevWordLevel.wordAtLevel period 6 (↑I.fst) I.snd ⋯) p)))

The external pressure commutator is the actual difference of two Sobolev coefficient products.

theorem EulerGevreyDifferentiatedEquation.basePressure_as_difference (period : ℝ) [Fact (0 < period)] {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) (N : ℕ) (hN : N + 6 ≤ s) (p : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (I : EulerGevreyMetricComparison.ExternalWord N) (a : EulerBaseWordMetric.BaseWord 6) : EulerGevreyForcingComponents.basePressureForcing period K0 N hN p I a = EulerCylinderSobolevSpace.value period ((EulerSobolevWordLevel.wordAtLevel period 0 (↑a.fst) a.snd ⋯) ((EulerSobolevCoefficientPressure.coefficientSobolevOperator period K0) ((EulerSobolevWordLevel.wordAtLevel period 6 (↑I.fst) I.snd ⋯) p))) - A.operator (EulerGevreyMetricComparison.energyValues period 6 N hN p I a)

The base pressure commutator is the actual differentiated product minus its top coefficient action.

theorem EulerGevreyDifferentiatedEquation.pressure_telescope (period : ℝ) [Fact (0 < period)] {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (K0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) (N : ℕ) (hN : N + 6 ≤ s) (p : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerGevreyForcingComponents.externalPressureForcing period K N hN p + EulerGevreyForcingComponents.basePressureForcing period K0 N hN p = EulerGevreyMetricComparison.energyValues period 6 N hN ((EulerSobolevCoefficientPressure.coefficientSobolevOperator period K) p) - fun (I : EulerGevreyMetricComparison.ExternalWord N) (a : EulerBaseWordMetric.BaseWord 6) => A.operator (EulerGevreyMetricComparison.energyValues period 6 N hN p I a)

External and base coefficient commutators telescope to the exact differentiated pressure term.

theorem EulerGevreyDifferentiatedEquation.correction_differentiated_identity (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (K0 : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) (N : ℕ) (hN : N + 6 ≤ s) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (f p0 p1 : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerGevreyMetricComparison.energyValues period 6 N hN (((EulerSobolevTransport.transportBilinear period hs L hL) u) v + f - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period K) p0 - (EulerSobolevCoefficientPressure.coefficientSobolevOperator period K) p1) = (topTransport period N hN L u v - fun (I : EulerGevreyMetricComparison.ExternalWord N) (a : EulerBaseWordMetric.BaseWord 6) => A.operator (EulerGevreyMetricComparison.energyValues period 6 N hN (p0 + p1) I a)) - EulerGevreyCorrectionForcing.correctionForcing period hs K K0 N hN L hL u v f p0 p1

The seven bounded forcing terms are exactly the remainder in the differentiated actual correction equation.