The actual differentiated correction forcing and its cutoff-independent nonlinear bound.

The genuine base transport commutator on finite Sobolev fields, with an H⁶-only bound.

The fixed-base transport commutator estimate with only H⁶ velocity norms.

noncomputable def EulerBaseTransportL2.baseTransportConstant (period : ℝ) [Fact (0 < period)] : ℝ

The base transport constant depends only on the fixed Sobolev index and cylinder period.

Equations

• EulerBaseTransportL2.baseTransportConstant period = 4 * 63 * 5460 * 1365 * EulerMixedH5Product.mixedConstant period

theorem EulerBaseTransportL2.baseTransportConstant_nonneg (period : ℝ) [Fact (0 < period)] : 0 ≤ baseTransportConstant period

theorem EulerBaseTransportL2.gradientFive_le_six (period : ℝ) [Fact (0 < period)] {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : EulerLiftedGradientSpace.LiftDomain period → F) : EulerBaseTransportCommutator.gradientFiveNorm period f ≤ 5460 * EulerCylinderSobolev.liftSobolevNorm period 6 f

The gradient H⁵ sum is controlled by the actual H⁶ norm with a fixed combinatorial factor.

theorem EulerBaseTransportL2.fieldL2_sum_le (period : ℝ) [Fact (0 < period)] {ι : Type u_1} {F : Type u_2} [NormedAddCommGroup F] (S : Finset ι) (f : ι → EulerLiftedGradientSpace.LiftDomain period → F) (hf : ∀ i ∈ S, MeasureTheory.MemLp (f i) 2 (EulerLiftedGradientSpace.liftMeasure period)) : (MeasureTheory.eLpNorm (∑ i ∈ S, f i) 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal ≤ ∑ i ∈ S, (MeasureTheory.eLpNorm (f i) 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal

Summing actual L² fields respects the sum of their finite L² norms.

theorem EulerBaseTransportL2.transport_base_L2 (period : ℝ) [Fact (0 < period)] {n : ℕ} (hn : n ≤ 6) (w : Fin n → Fin 4) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (f g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL : ∀ (j : ℕ) (a : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period a f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL : ∀ (j : ℕ) (a : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period a g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : MeasureTheory.MemLp (EulerExternalTransportCommutator.transportCommutator period w (⇑(EulerFunctionalVelocity.velocityMap L) ∘ f) g) 2 (EulerLiftedGradientSpace.liftMeasure period) ∧ (MeasureTheory.eLpNorm (EulerExternalTransportCommutator.transportCommutator period w (⇑(EulerFunctionalVelocity.velocityMap L) ∘ f) g) 2 (EulerLiftedGradientSpace.liftMeasure period)).toReal ≤ baseTransportConstant period * EulerCylinderSobolev.liftSobolevNorm period 6 f * EulerCylinderSobolev.liftSobolevNorm period 6 g

The literal transport commutator through six base derivatives is in L² and bounded using only the two H⁶ norms.

Genuine transport as a bounded bilinear map from Sobolev velocity and an H¹ transported field into L².

noncomputable def EulerTransportL2Bilinear.transportL2Bilinear (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period 1) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

The actual product of a bounded Sobolev velocity with the genuine first derivatives of an H¹ field.

Equations

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

theorem EulerTransportL2Bilinear.transportL2Bilinear_apply (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) : ((transportL2Bilinear period hq L) u) e = ∑ i : Fin 4, EulerSobolevL2Product.scalarProduct period hq (L i) u (EulerCylinderSobolevSpace.value period ((EulerCylinderSobolevSpace.derivativeOperator period 0 i) e))

Transport is the sum of its four literal scalar-times-derivative L² products.

theorem EulerTransportL2Bilinear.transportL2Bilinear_eq_metric (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) : ((transportL2Bilinear period hq (EulerSobolevTransport.velocityComponents κ m)) u) e = (EulerSobolevMetricTransport.transportOperator period hq κ m u) e

On the actual lifted velocity coefficients, this is exactly the operator used in metric transport cancellation.

theorem EulerTransportL2Bilinear.transportL2Bilinear_ae (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 3 ≤ q) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (e : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)) (f g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (he : ↑↑(EulerCylinderSobolevSpace.value period e) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) : ↑↑(((transportL2Bilinear period hq L) u) e) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] EulerH6Nonlinear.transportField period 3 (⇑(EulerFunctionalVelocity.velocityMap L) ∘ f) g

The bilinear L² transport agrees almost everywhere with the actual classical directional transport.

Transfer of continuous real inequalities from actual smooth H∞ representatives to finite Sobolev fields.

theorem EulerSmoothInequalityTransfer.binary_le_of_smooth (period : ℝ) [Fact (0 < period)] {q : ℕ} (F G : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) × ↥(EulerCylinderSobolevSpace.SobolevSpace period q) → ℝ) (hF : Continuous F) (hG : Continuous G) (hbound : ∀ (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (f g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3), ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f → ↑↑(EulerCylinderSobolevSpace.value period v) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g → (∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) → (∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) → (∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2 (EulerLiftedGradientSpace.liftMeasure period)) → (∀ (j : ℕ) (w : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w g) 2 (EulerLiftedGradientSpace.liftMeasure period)) → F (u, v) ≤ G (u, v)) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : F (u, v) ≤ G (u, v)

Every continuous inequality proved for actual smooth H∞ representatives passes to the genuine finite Sobolev space.

@[instance_reducible]

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

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

Equations

• EulerSobolevBaseCommutator.baseCommGroup period q = inferInstance

@[instance_reducible]

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

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

Equations

• EulerSobolevBaseCommutator.baseCommSpace period q = inferInstance

noncomputable def EulerSobolevBaseCommutator.baseCommutator (period : ℝ) [Fact (0 < period)] (r : ℕ) (hr : r ≤ 6) (w : Fin r → Fin 4) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) : ↥(EulerCylinderSobolevSpace.SobolevSpace period 7) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period 7) →L[ℝ] ↥(EulerLiftedGradientSpace.LiftL2 period)

The actual base derivative commutator, evaluated in L² on its genuine H⁷ domain.

Equations

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

theorem EulerSobolevBaseCommutator.baseCommutator_apply (period : ℝ) [Fact (0 < period)] (r : ℕ) (hr : r ≤ 6) (w : Fin r → Fin 4) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period 7)) : ((baseCommutator period r hr w L hL) u) v = EulerCylinderSobolevSpace.value period ((EulerSobolevWordLevel.wordAtLevel period 0 r w hr) (((EulerSobolevTransport.transportBilinear period baseCommutator._proof_1 L hL) u) v)) - ((EulerTransportL2Bilinear.transportL2Bilinear period baseCommutator._proof_2 L) u) ((EulerSobolevWordLevel.wordAtLevel period 1 r w ⋯) v)

The actual operands of the finite-Sobolev base commutator.

theorem EulerSobolevBaseCommutator.baseCommutator_ae (period : ℝ) [Fact (0 < period)] (r : ℕ) (hr : r ≤ 6) (w : Fin r → Fin 4) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period 7)) (f g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hv : ↑↑(EulerCylinderSobolevSpace.value period v) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) : ↑↑(((baseCommutator period r hr w L hL) u) v) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] EulerExternalTransportCommutator.transportCommutator period w (⇑(EulerFunctionalVelocity.velocityMap L) ∘ f) g

Its actual L² representative is the literal classical base derivative commutator.

theorem EulerSobolevBaseCommutator.baseCommutator_smooth_bound (period : ℝ) [Fact (0 < period)] (r : ℕ) (hr : r ≤ 6) (w : Fin r → Fin 4) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period 7)) (f g : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hu : ↑↑(EulerCylinderSobolevSpace.value period u) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] f) (hv : ↑↑(EulerCylinderSobolevSpace.value period v) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] g) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (hfL : ∀ (j : ℕ) (a : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period a f) 2 (EulerLiftedGradientSpace.liftMeasure period)) (hgL : ∀ (j : ℕ) (a : Fin j → Fin 4), MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period a g) 2 (EulerLiftedGradientSpace.liftMeasure period)) : ‖((baseCommutator period r hr w L hL) u) v‖ ≤ EulerBaseTransportL2.baseTransportConstant period * EulerCylinderSobolevSpace.sumNorm period ((EulerCylinderSobolevSpace.restrictOperator period baseCommutator_smooth_bound._proof_1) u) * EulerCylinderSobolevSpace.sumNorm period ((EulerCylinderSobolevSpace.restrictOperator period baseCommutator_smooth_bound._proof_1) v)

On actual smooth representatives, the base commutator has the H⁶-only norm bound.

theorem EulerSobolevBaseCommutator.baseCommutator_bound (period : ℝ) [Fact (0 < period)] (r : ℕ) (hr : r ≤ 6) (w : Fin r → Fin 4) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period 7)) : ‖((baseCommutator period r hr w L hL) u) v‖ ≤ EulerBaseTransportL2.baseTransportConstant period * EulerCylinderSobolevSpace.sumNorm period ((EulerCylinderSobolevSpace.restrictOperator period baseCommutator_smooth_bound._proof_1) u) * EulerCylinderSobolevSpace.sumNorm period ((EulerCylinderSobolevSpace.restrictOperator period baseCommutator_smooth_bound._proof_1) v)

The genuine finite-Sobolev base commutator satisfies the same H⁶-only estimate, with no smoothness hypothesis.

Summation of the actual base transport commutators with no external-cutoff constant.

theorem EulerGevreyBaseTransport.restrict_wordAtLevel (period : ℝ) [Fact (0 < period)] {s p q n : ℕ} (hq : q ≤ p) (w : Fin n → Fin 4) (hp : n + p ≤ s) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : (EulerCylinderSobolevSpace.restrictOperator period hq) ((EulerSobolevWordLevel.wordAtLevel period p n w hp) u) = (EulerSobolevWordLevel.wordAtLevel period q n w ⋯) u

Restriction commutes with taking an actual derivative word at a lower Sobolev level.

theorem EulerGevreyBaseTransport.sumNorm_restrict_le_weighted (period : ℝ) [Fact (0 < period)] {s q : ℕ} (hq : q ≤ s) (N : ℕ) (ρ : ℝ) (hρ : 0 < ρ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerCylinderSobolevSpace.sumNorm period ((EulerCylinderSobolevSpace.restrictOperator period hq) u) ≤ EulerSobolevGevreyOperators.weightedNorm period q N ρ u

The exact base derivative sum is contained in every truncated actual Gevrey norm.

theorem EulerGevreyBaseTransport.weighted_word_sums (period : ℝ) [Fact (0 < period)] {s : ℕ} (q N : ℕ) (hN : N + q ≤ s) (ρ : ℝ) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : ∑ I : EulerGevreyMetricComparison.ExternalWord N, EulerPacketWeights.weight ρ ↑I.fst * EulerCylinderSobolevSpace.sumNorm period ((EulerSobolevWordLevel.wordAtLevel period q (↑I.fst) I.snd ⋯) u) = EulerSobolevGevreyOperators.weightedNorm period q N ρ u

Exact external-word expansion of the actual Gevrey Sobolev sum.

noncomputable def EulerGevreyBaseTransport.baseTransportForcing (period : ℝ) [Fact (0 < period)] {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))) : EulerGevreyMetricComparison.ExternalWord N → EulerBaseWordMetric.BaseWord 6 → ↥(EulerLiftedGradientSpace.LiftL2 period)

The literal base transport forcing at every external and base derivative word.

Equations

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

theorem EulerGevreyBaseTransport.baseTransportForcing_family_bound (period : ℝ) [Fact (0 < period)] {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))) (I : EulerGevreyMetricComparison.ExternalWord N) : EulerFiniteMetricEnergy.familyNorm (baseTransportForcing period N hN L hL u v I) ≤ 5461 * EulerBaseTransportL2.baseTransportConstant period * EulerCylinderSobolevSpace.sumNorm period ((EulerCylinderSobolevSpace.restrictOperator period ⋯) u) * EulerCylinderSobolevSpace.sumNorm period ((EulerSobolevWordLevel.wordAtLevel period 6 (↑I.fst) I.snd ⋯) v)

Each base-word forcing family is controlled by the fixed H⁶ norms, with the fixed word-count factor 5461.

theorem EulerGevreyBaseTransport.baseTransportForcing_weighted_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : EulerWeightedCylinderEnergy.weightedForcingSum ρ (fun (I : EulerGevreyMetricComparison.ExternalWord N) => ↑I.fst) (baseTransportForcing period N hN L hL u v) ≤ 5461 * EulerBaseTransportL2.baseTransportConstant period * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ v

The actual weighted base transport forcing has no external derivative loss or cutoff-dependent coefficient.

Literal differentiated forcing arrays and their actual finite Gevrey norms.

theorem EulerGevreyForcingComponents.forcing_le_jetSum (period : ℝ) [Fact (0 < period)] {ι : Type u_1} [Fintype ι] (order : ι → ℕ) (ρ : ℝ) (hρ : 0 < ρ) (f : ι → ↥(EulerLiftedGradientSpace.LiftL2 period)) (J : (i : ι) → EulerSpatialSobolevInverse.SpatialJet period EulerCylinderSobolev.standardDirection 6 (f i)) : (EulerWeightedCylinderEnergy.weightedForcingSum ρ order fun (i : ι) => EulerBaseWordMetric.baseWordValues period (J i)) ≤ ∑ i : ι, EulerPacketWeights.weight ρ (order i) * (J i).sobolevNorm

A finite family of actual base-word derivatives is controlled by its genuine derivative-sum norm.

theorem EulerGevreyForcingComponents.sourceForcing_weighted_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (f : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerWeightedCylinderEnergy.weightedForcingSum ρ (fun (I : EulerGevreyMetricComparison.ExternalWord N) => ↑I.fst) (EulerGevreyMetricComparison.energyValues period 6 N hN f) ≤ EulerSobolevGevreyOperators.weightedNorm period 6 N ρ f

The actual differentiated order-zero source is controlled by its finite weighted Sobolev norm.

noncomputable def EulerGevreyForcingComponents.externalTransportForcing (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))) : EulerGevreyMetricComparison.ExternalWord N → EulerBaseWordMetric.BaseWord 6 → ↥(EulerLiftedGradientSpace.LiftL2 period)

The literal base derivatives of the external transport commutator.

Equations

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

theorem EulerGevreyForcingComponents.externalTransportForcing_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} (hs : 6 ≤ s) (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) : EulerWeightedCylinderEnergy.weightedForcingSum ρ (fun (I : EulerGevreyMetricComparison.ExternalWord N) => ↑I.fst) (externalTransportForcing period hs N hN L hL u v) ≤ EulerSobolevTransportCommutator.weightedCommutatorNorm period hs N hN ρ L hL u v

The actual external transport forcing is bounded by the already proved commutator norm.

noncomputable def EulerGevreyForcingComponents.externalPressureForcing (period : ℝ) [Fact (0 < period)] {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (N : ℕ) (hN : N + 6 ≤ s) (p : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerGevreyMetricComparison.ExternalWord N → EulerBaseWordMetric.BaseWord 6 → ↥(EulerLiftedGradientSpace.LiftL2 period)

The literal base derivatives of the actual external coefficient-pressure commutator.

Equations

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

theorem EulerGevreyForcingComponents.externalPressureForcing_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection s A) (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (p : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerWeightedCylinderEnergy.weightedForcingSum ρ (fun (I : EulerGevreyMetricComparison.ExternalWord N) => ↑I.fst) (externalPressureForcing period K N hN p) ≤ EulerGevreyPressureEnergy.externalPressureNorm period K N ρ p

The actual differentiated external pressure forcing is controlled by its proved H⁶ commutator sum.

theorem EulerGevreyForcingComponents.sobolevSize_order_zero (period : ℝ) [Fact (0 < period)] (f : ↥(EulerLiftedGradientSpace.LiftL2 period)) : EulerH6Pressure.sobolevSize period 0 f = ‖f‖

At order zero the genuine Sobolev size is exactly the L² norm.

noncomputable def EulerGevreyForcingComponents.basePressureForcing (period : ℝ) [Fact (0 < period)] {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) (N : ℕ) (hN : N + 6 ≤ s) (p : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerGevreyMetricComparison.ExternalWord N → EulerBaseWordMetric.BaseWord 6 → ↥(EulerLiftedGradientSpace.LiftL2 period)

The literal base derivative commutator of G with each external pressure derivative.

Equations

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

theorem EulerGevreyForcingComponents.basePressureForcing_family_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) (N : ℕ) (hN : N + 6 ≤ s) (p : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) (I : EulerGevreyMetricComparison.ExternalWord N) : EulerFiniteMetricEnergy.familyNorm (basePressureForcing period K N hN p I) ≤ ∑ r ∈ Finset.range 7, EulerH6Pressure.commutatorBlock K (EulerH6Pressure.SpatialJet.derivativeJet (EulerCylinderSobolevSpace.toJet period p) I.snd ⋯) 0 r

At each external word, summing the actual base commutator norms gives the base-pressure block expression.

theorem EulerGevreyForcingComponents.basePressureForcing_bound (period : ℝ) [Fact (0 < period)] {s : ℕ} {A : EulerSpatialSobolevInverse.SmoothCoefficient period} (K : EulerSpatialSobolevInverse.CoefficientJet period EulerCylinderSobolev.standardDirection 6 A) (N : ℕ) (hN : N + 6 ≤ s) (ρ : ℝ) (hρ : 0 < ρ) (p : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerWeightedCylinderEnergy.weightedForcingSum ρ (fun (I : EulerGevreyMetricComparison.ExternalWord N) => ↑I.fst) (basePressureForcing period K N hN p) ≤ EulerGevreyPressureEnergy.basePressureNorm period K N hN ρ p

The actual base pressure forcing is controlled by the previously proved lower-order pressure commutator norm.

noncomputable def EulerGevreyCorrectionForcing.correctionForcing (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.ExternalWord N → EulerBaseWordMetric.BaseWord 6 → ↥(EulerLiftedGradientSpace.LiftL2 period)

The seven literal commutator/source terms after external and base differentiation of equation (17). The two pressure arguments are the positive projected inverses; the PDE pressure has the opposite sign.

Equations

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

theorem EulerGevreyCorrectionForcing.forcing_seven_le {α : Type u_1} {β : Type u_2} {H : Type u_3} [Fintype α] [Fintype β] [NormedAddCommGroup H] (ρ : ℝ) (hρ : 0 < ρ) (order : α → ℕ) (a b c d e f g : α → β → H) : EulerWeightedCylinderEnergy.weightedForcingSum ρ order (a + b + c + d + e + f + g) ≤ EulerWeightedCylinderEnergy.weightedForcingSum ρ order a + EulerWeightedCylinderEnergy.weightedForcingSum ρ order b + EulerWeightedCylinderEnergy.weightedForcingSum ρ order c + EulerWeightedCylinderEnergy.weightedForcingSum ρ order d + EulerWeightedCylinderEnergy.weightedForcingSum ρ order e + EulerWeightedCylinderEnergy.weightedForcingSum ρ order f + EulerWeightedCylinderEnergy.weightedForcingSum ρ order g

The triangle inequality for seven actual forcing arrays has coefficient one.

theorem EulerGevreyCorrectionForcing.correctionForcing_raw_bound (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) (ρ : ℝ) (hρ : 0 < ρ) (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)) : EulerWeightedCylinderEnergy.weightedForcingSum ρ (fun (I : EulerGevreyMetricComparison.ExternalWord N) => ↑I.fst) (correctionForcing period hs K K0 N hN L hL u v f p0 p1) ≤ EulerSobolevGevreyOperators.weightedNorm period 6 N ρ f + 4 * EulerH6Nonlinear.productConstant period 3 * ρ⁻¹ * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u * EulerSobolevTransportCommutator.weightedLoss period 6 N ρ v + 5461 * EulerBaseTransportL2.baseTransportConstant period * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ v + EulerGevreyPressureEnergy.externalPressureNorm period K N ρ p0 + EulerGevreyPressureEnergy.basePressureNorm period K0 N hN ρ p0 + EulerGevreyPressureEnergy.externalPressureNorm period K N ρ p1 + EulerGevreyPressureEnergy.basePressureNorm period K0 N hN ρ p1

All actual forcing components satisfy their derived bounds on finite Sobolev fields.

theorem EulerGevreyCorrectionForcing.correctionForcing_bound (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) (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (c : ℝ) (hc : 0 < c) (hpos : ∀ (x : EulerLiftedGradientSpace.LiftDomain period) (v : EulerLiftedGradientSpace.Vector3), c * ‖v‖ ^ 2 ≤ inner ℝ ((A.coefficient x) v) v) (N : ℕ) (hN : N + 6 ≤ s) (ρ Rc M : ℝ) (hρ : 0 < ρ) (hRc : 0 ≤ Rc) (hM : 1 ≤ M) (hbase5 : (EulerH6Pressure.CoefficientJet.restrict K 5 ⋯).pressureConstant c ≤ M) (hbase6 : (EulerH6Pressure.CoefficientJet.restrict K 6 hs).pressureConstant c ≤ M) (hsmall : 4 * M * (ρ * Rc) ≤ 1) (hcoeff : ∀ (l : ℕ), 1 ≤ l → l ≤ N → EulerH6Pressure.coefficientBlock period K 6 l ≤ Rc ^ l * ↑l.factorial ^ 2) (L : Fin 4 → EulerLiftedGradientSpace.Vector3 →L[ℝ] ℝ) (hL : ∀ (i : Fin 4), ‖L i‖ ≤ 1) (u v : ↥(EulerCylinderSobolevSpace.SobolevSpace period (s + 1))) (f : ↥(EulerCylinderSobolevSpace.SobolevSpace period s)) : EulerWeightedCylinderEnergy.weightedForcingSum ρ (fun (I : EulerGevreyMetricComparison.ExternalWord N) => ↑I.fst) (correctionForcing period hs K K0 N hN L hL u v f ((EulerSobolevCoefficientPressure.pressureSobolevOperator period K κ m c hc hpos) f) (EulerGevreyPressureTransport.transportPressure period hs K κ m c hc hpos L hL u v)) ≤ (1 + 2 * M * (EulerSobolevGevreyOperators.weightedCoefficient period K 6 N ρ + 448 * EulerBasePressureCommutator.baseCoefficientSum period K0)) * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ f + (5461 * EulerBaseTransportL2.baseTransportConstant period + 448 * EulerBasePressureCommutator.baseCoefficientSum period K0 * (8 * M * (5460 * EulerH6Nonlinear.lowerProductConstant period 3))) * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ v + (4 * EulerH6Nonlinear.productConstant period 3 * ρ⁻¹ + 32 * Rc * M * EulerH6Nonlinear.productConstant period 3) * EulerSobolevGevreyOperators.weightedNorm period 6 N ρ u * EulerSobolevTransportCommutator.weightedLoss period 6 N ρ v

The full actual forcing with both genuine projected pressure solves obeys the spatial part of equation (19). Every velocity derivative in the bound lies at or below the chosen cutoff.