Actual gradient-supremum control of Euler Sobolev norms. The gradient norm is a constructed continuous path, its time integral controls H³, and the checked H³-tame estimate then propagates every higher order on the same time interval.

Sharp H³ products controlled by the actual velocity gradient. The only middle product is D²u D²u, handled by cubic testing.

The sharp middle-derivative interpolation needed by H³ Euler energy. Everything is an actual smooth L² field. Cubic testing and noncompact integration by parts prove the L⁴ inequality without a support or interpolation hypothesis.

theorem EulerOrdinarySobolev.scalarProduct_norm_square (A B : EulerLpTranslation.SmoothL2Field ℝ) : ‖(scalarProduct A B).toLp‖ ^ 2 = inner ℝ (scalarProduct A A).toLp (scalarProduct B B).toLp

theorem EulerOrdinarySobolev.directional_square_identity (A : EulerLpTranslation.SmoothL2Field ℝ) (v : EulerSmoothLimit.Space) : ‖(scalarProduct (A.directionalField v) (A.directionalField v)).toLp‖ ^ 2 = -3 * inner ℝ (scalarProduct A (scalarProduct (A.directionalField v) (A.directionalField v))).toLp ((A.directionalField v).directionalField v).toLp

theorem EulerOrdinarySobolev.directional_square_norm (A : EulerLpTranslation.SmoothL2Field ℝ) (v : EulerSmoothLimit.Space) (K : ℝ) (hK : ∀ (x : EulerSmoothLimit.Space), ‖A.field x‖ ≤ K) : ‖(scalarProduct (A.directionalField v) (A.directionalField v)).toLp‖ ≤ 3 * K * ‖((A.directionalField v).directionalField v).toLp‖

theorem EulerOrdinarySobolev.scalarProduct_norm_of_square_bounds (A B : EulerLpTranslation.SmoothL2Field ℝ) (C : ℝ) (hC : 0 ≤ C) (hA : ‖(scalarProduct A A).toLp‖ ≤ C) (hB : ‖(scalarProduct B B).toLp‖ ≤ C) : ‖(scalarProduct A B).toLp‖ ≤ C

theorem EulerOrdinarySobolev.firstWord_pointwise_gradient (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K : ℝ) (hK : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ A.field x‖ ≤ K) (w : Fin 1 → Fin 3) (x : EulerSmoothLimit.Space) : ‖(wordField A w).field x‖ ≤ K

theorem EulerOrdinarySobolev.secondWord_square_gradient (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K N : ℝ) (hK : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ A.field x‖ ≤ K) (hN : WordBound 3 N A) (w : Fin 2 → Fin 3) (i : Fin 3) : ‖(scalarProduct (wordField (EulerLpTranslation.SmoothL2Field.mapField (EuclideanSpace.proj i) A) w) (wordField (EulerLpTranslation.SmoothL2Field.mapField (EuclideanSpace.proj i) A) w)).toLp‖ ≤ 3 * K * N

theorem EulerOrdinarySobolev.scalar_secondWord_product_gradient (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K N : ℝ) (hK : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ A.field x‖ ≤ K) (hN : WordBound 3 N A) (w v : Fin 2 → Fin 3) (i j : Fin 3) : ‖(scalarProduct (wordField (EulerLpTranslation.SmoothL2Field.mapField (EuclideanSpace.proj i) A) w) (wordField (EulerLpTranslation.SmoothL2Field.mapField (EuclideanSpace.proj j) A) v)).toLp‖ ≤ 3 * K * N

theorem EulerOrdinarySobolev.norm_le_sum_coordinates (x : EulerSmoothLimit.Space) : ‖x‖ ≤ ∑ i : Fin 3, ‖x.ofLp i‖

theorem EulerOrdinarySobolev.secondWord_product_gradient (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K N : ℝ) (hK : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ A.field x‖ ≤ K) (hN : WordBound 3 N A) (w v : Fin 2 → Fin 3) (i : Fin 3) : ‖(coordinateProduct i (wordField A w) (wordField A v)).toLp‖ ≤ 9 * K * N

theorem EulerOrdinarySobolev.coordinateProduct_gradient (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K N : ℝ) (hK : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ A.field x‖ ≤ K) (hN : WordBound 3 N A) {k l : ℕ} (hk : 1 ≤ k) (hl : 1 ≤ l) (hkl : k + l ≤ 4) (w : Fin k → Fin 3) (v : Fin l → Fin 3) (i : Fin 3) : ‖(coordinateProduct i (wordField A w) (wordField A v)).toLp‖ ≤ 9 * K * N

theorem EulerOrdinarySobolev.gradient_tame_outer_product (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K N : ℝ) (hK : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ A.field x‖ ≤ K) (hN : WordBound 3 N A) {n k l : ℕ} (hk : 1 ≤ k) (hl : 1 ≤ l) (horder : n + k + l ≤ 4) (a : Fin n → Fin 3) (w : Fin k → Fin 3) (v : Fin l → Fin 3) (i : Fin 3) : ‖(wordField (coordinateProduct i (wordField A w) (wordField A v)) a).toLp‖ ≤ 2 ^ n * 9 * K * N

Sharp H³ transport energy with the actual L-infinity norm of the velocity gradient. The pressure and undifferentiated transport cancel before the cubic-test interpolation estimate is used.

theorem EulerOrdinarySobolev.gradientSup_advection_outer (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K N : ℝ) (hK : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ A.field x‖ ≤ K) (hN : WordBound 3 N A) {n k l : ℕ} (hk : 1 ≤ k) (horder : n + k + l ≤ 3) (a : Fin n → Fin 3) (w : Fin k → Fin 3) (v : Fin l → Fin 3) : ‖(wordField (advectionField (wordField A w) (wordField A v)) a).toLp‖ ≤ 27 * 2 ^ n * K * N

theorem EulerOrdinarySobolev.gradient_transportCommutator_word (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K N : ℝ) (hK : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ A.field x‖ ≤ K) (hN : WordBound 3 N A) {n l : ℕ} (horder : n + l ≤ 3) (a : Fin n → Fin 3) (v : Fin l → Fin 3) : ‖(transportCommutator A (wordField A v) a).toLp‖ ≤ 27 * (2 ^ n - 1) * K * N

theorem EulerOrdinarySobolev.gradient_transportCommutator (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K N : ℝ) (hK : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ A.field x‖ ≤ K) (hN : WordBound 3 N A) {n : ℕ} (hn : n ≤ 3) (w : Fin n → Fin 3) : ‖(transportCommutator A A w).toLp‖ ≤ 27 * (2 ^ n - 1) * K * N

def EulerOrdinarySobolev.gradientEnergyConstant : ℝ

Gradient energy constant, given by 54*(∑ n ∈ range 4, (6 : ℝ)^n).

Equations

• EulerOrdinarySobolev.gradientEnergyConstant = 54 * ∑ n ∈ Finset.range 4, 6 ^ n

theorem EulerOrdinarySobolev.gradientEnergyConstant_nonneg : 0 ≤ gradientEnergyConstant

theorem EulerOrdinarySobolev.gradientEnergyConstant_eq : gradientEnergyConstant = 13986

theorem EulerOrdinarySobolev.eulerRhs_word_gradient (A P : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K : ℝ) (hK : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ A.field x‖ ≤ K) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence A.field x = 0) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (hP : P.toLp ∈ EulerMeanSolenoidal.gradientSpace) {n : ℕ} (hn : n ≤ 3) (w : Fin n → Fin 3) : inner ℝ (wordField A w).toLp (wordField (eulerRhs A P) w).toLp ≤ 27 * 2 ^ n * K * wordEnergy 3 A

theorem EulerOrdinarySobolev.h3_energy_gradient (A P : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (K : ℝ) (hK : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ A.field x‖ ≤ K) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence A.field x = 0) (hA : A.toLp ∈ EulerMeanSolenoidal.solenoidalSpace) (hP : P.toLp ∈ EulerMeanSolenoidal.gradientSpace) : integerEnergyProduction 3 A (eulerRhs A P) ≤ gradientEnergyConstant * K * wordEnergy 3 A

noncomputable def EulerOrdinarySobolev.Evolution.gradientNormPath {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) : C(↑(Set.Icc 0 T), ℝ)

Gradient norm path as an element of C(Icc (0 : ℝ) T,ℝ).

Equations

• U.gradientNormPath = { toFun := fun (t : ↑(Set.Icc 0 T)) => ‖EulerMeanSobolevBoundedField.finiteField (U.velocity t).derivative‖, continuous_toFun := ⋯ }

theorem EulerOrdinarySobolev.Evolution.gradientNormPath_nonneg {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) : 0 ≤ U.gradientNormPath t

theorem EulerOrdinarySobolev.Evolution.gradientNormPath_le_iff {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) (K : ℝ) : U.gradientNormPath t ≤ K ↔ ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (U.velocity t).field x‖ ≤ K

theorem EulerOrdinarySobolev.Evolution.pointwise_gradient_le {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) : ‖fderiv ℝ (U.velocity t).field x‖ ≤ U.gradientNormPath t

noncomputable def EulerOrdinarySobolev.Evolution.gradientIntegral {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) : ℝ

Gradient integral, given by realIntegral T hT U.gradientNormPath t.

Equations

• U.gradientIntegral t = EulerContinuousTimeIntegral.realIntegral T hT U.gradientNormPath ↑t

theorem EulerOrdinarySobolev.Evolution.gradientIntegral_nonneg {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) : 0 ≤ U.gradientIntegral t

theorem EulerOrdinarySobolev.Evolution.gradientIntegral_le_const {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (K : ℝ) (hK : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (U.velocity t).field x‖ ≤ K) (t : ↑(Set.Icc 0 T)) : U.gradientIntegral t ≤ K * ↑t

theorem EulerOrdinarySobolev.Evolution.integerEnergyDerivative_gradient {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (K : ℝ) (t : ↑(Set.Icc 0 T)) (hK : ∀ (x : EulerSmoothLimit.Space), ‖fderiv ℝ (U.velocity t).field x‖ ≤ K) : U.integerEnergyDerivative 3 t ≤ gradientEnergyConstant * K * (U.integerEnergyPath 3) t

theorem EulerOrdinarySobolev.Evolution.h3_energy_gradientIntegral {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (t : ↑(Set.Icc 0 T)) : wordEnergy 3 (U.velocity t) ≤ wordEnergy 3 (U.velocity ⟨0, ⋯⟩) * Real.exp (gradientEnergyConstant * U.gradientIntegral t)

theorem EulerOrdinarySobolev.Evolution.h3_energy_gradient_bound {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (K : ℝ) (hK : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (U.velocity t).field x‖ ≤ K) (t : ↑(Set.Icc 0 T)) : wordEnergy 3 (U.velocity t) ≤ wordEnergy 3 (U.velocity ⟨0, ⋯⟩) * Real.exp (gradientEnergyConstant * K * ↑t)

noncomputable def EulerOrdinarySobolev.Evolution.gradientH3Bound {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (G : ℝ) : ℝ

Gradient H3 bound, given by Real.sqrt (wordEnergy 3 (U.velocity ⟨0,le_rfl,hT⟩)*Real.exp (gradientEnergyConstant*G)).

Equations

• U.gradientH3Bound G = √(EulerOrdinarySobolev.wordEnergy 3 (U.velocity ⟨0, ⋯⟩) * Real.exp (EulerOrdinarySobolev.gradientEnergyConstant * G))

theorem EulerOrdinarySobolev.Evolution.wordBound_of_gradientIntegral {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (G : ℝ) (hG : ∀ (t : ↑(Set.Icc 0 T)), U.gradientIntegral t ≤ G) (t : ↑(Set.Icc 0 T)) : WordBound 3 (U.gradientH3Bound G) (U.velocity t)

theorem EulerOrdinarySobolev.Evolution.h3_tensorNorm_of_gradientIntegral {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (G : ℝ) (hG : ∀ (t : ↑(Set.Icc 0 T)), U.gradientIntegral t ≤ G) (t : ↑(Set.Icc 0 T)) : tensorNorm 3 (U.velocity t) ≤ wordCount 3 * U.gradientH3Bound G

theorem EulerOrdinarySobolev.Evolution.higher_energy_of_gradientIntegral {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (m : ℕ) (hm : 3 ≤ m) (G : ℝ) (hG : ∀ (t : ↑(Set.Icc 0 T)), U.gradientIntegral t ≤ G) (t : ↑(Set.Icc 0 T)) : wordEnergy m (U.velocity t) ≤ wordEnergy m (U.velocity ⟨0, ⋯⟩) * Real.exp (tameEnergyConstant m * U.gradientH3Bound G * T)

theorem EulerOrdinarySobolev.Evolution.higher_tensorNorm_of_gradientIntegral {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (m : ℕ) (hm : 3 ≤ m) (G : ℝ) (hG : ∀ (t : ↑(Set.Icc 0 T)), U.gradientIntegral t ≤ G) (t : ↑(Set.Icc 0 T)) : tensorNorm m (U.velocity t) ≤ wordCount m * √(wordEnergy m (U.velocity ⟨0, ⋯⟩) * Real.exp (tameEnergyConstant m * U.gradientH3Bound G * T))

theorem EulerOrdinarySobolev.Evolution.higher_tensorNorm_of_gradientBound {T : ℝ} {hT : 0 ≤ T} (U : Evolution T hT) (m : ℕ) (hm : 3 ≤ m) (K : ℝ) (hK : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (U.velocity t).field x‖ ≤ K) (t : ↑(Set.Icc 0 T)) : tensorNorm m (U.velocity t) ≤ wordCount m * √(wordEnergy m (U.velocity ⟨0, ⋯⟩) * Real.exp (tameEnergyConstant m * U.gradientH3Bound (K * T) * T))