The actual transport forcing has the shifted Gevrey H⁶ estimate without a cutoff-plus-one loss.
theorem
EulerH6Nonlinear.word_zero
(period : ℝ)
{F : Type u_1}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{n : ℕ}
(w : Fin n → Fin 4)
:
@[simp]
theorem
EulerH6Nonlinear.wordSobolevNorm_zero_field
(period : ℝ)
[Fact (0 < period)]
{F : Type u_1}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
(q n : ℕ)
:
theorem
EulerH6Nonlinear.smooth_sum
(period : ℝ)
{F : Type u_1}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{α : Type u_2}
(s : Finset α)
(f : α → EulerLiftedGradientSpace.LiftDomain period → F)
(hf :
∀ i ∈ s,
∀ (x : EulerLiftedGradientSpace.LiftDomain period),
ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (f i) x))
(x : EulerLiftedGradientSpace.LiftDomain period)
:
ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (∑ i ∈ s, f i) x)
theorem
EulerH6Nonlinear.word_sum
(period : ℝ)
{F : Type u_1}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{α : Type u_2}
(s : Finset α)
(f : α → EulerLiftedGradientSpace.LiftDomain period → F)
(hf :
∀ i ∈ s,
∀ (x : EulerLiftedGradientSpace.LiftDomain period),
ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (f i) x))
{n : ℕ}
(w : Fin n → Fin 4)
:
EulerCylinderSobolev.iteratedFieldDerivative period w (∑ i ∈ s, f i) = ∑ i ∈ s, EulerCylinderSobolev.iteratedFieldDerivative period w (f i)
theorem
EulerH6Nonlinear.sum_all_memLp
(period : ℝ)
[Fact (0 < period)]
{F : Type u_1}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{α : Type u_2}
(s : Finset α)
(f : α → EulerLiftedGradientSpace.LiftDomain period → F)
(hf :
∀ i ∈ s,
∀ (x : EulerLiftedGradientSpace.LiftDomain period),
ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (f i) x))
(hfL2 :
∀ i ∈ s,
∀ (j : ℕ) (w : Fin j → Fin 4),
MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w (f i)) 2
(EulerLiftedGradientSpace.liftMeasure period))
(j : ℕ)
(w : Fin j → Fin 4)
:
MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w (∑ i ∈ s, f i)) 2
(EulerLiftedGradientSpace.liftMeasure period)
theorem
EulerH6Nonlinear.wordSobolevNorm_sum_le
(period : ℝ)
[Fact (0 < period)]
{F : Type u_1}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
{α : Type u_2}
(s : Finset α)
(q n : ℕ)
(f : α → EulerLiftedGradientSpace.LiftDomain period → F)
(hf :
∀ i ∈ s,
∀ (x : EulerLiftedGradientSpace.LiftDomain period),
ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (f i) x))
(hfL2 :
∀ i ∈ s,
∀ (j : ℕ) (w : Fin j → Fin 4),
MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w (f i)) 2
(EulerLiftedGradientSpace.liftMeasure period))
:
theorem
EulerH6Nonlinear.wordSobolevNorm_postcomp_le
(period : ℝ)
[Fact (0 < period)]
{F : Type u_1}
{G : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
(q n : ℕ)
(L : F →L[ℝ] G)
(hL : ‖L‖ ≤ 1)
(f : EulerLiftedGradientSpace.LiftDomain period → F)
(hf :
∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x))
(hfL2 :
∀ (j : ℕ) (w : Fin j → Fin 4),
MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2
(EulerLiftedGradientSpace.liftMeasure period))
:
noncomputable def
EulerH6Nonlinear.transportField
(period : ℝ)
(q : ℕ)
(b : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain 4)
(e : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain q)
:
Actual transport in the four cylinder coordinates; angle is the first coordinate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerH6Nonlinear.transport_all_memLp
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
(b : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain 4)
(e : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain q)
(hb :
∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period b x))
(he :
∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period e x))
(hbL2 :
∀ (j : ℕ) (w : Fin j → Fin 4),
MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w b) 2
(EulerLiftedGradientSpace.liftMeasure period))
(heL2 :
∀ (j : ℕ) (w : Fin j → Fin 4),
MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w e) 2
(EulerLiftedGradientSpace.liftMeasure period))
(j : ℕ)
(w : Fin j → Fin 4)
:
MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w (transportField period q b e)) 2
(EulerLiftedGradientSpace.liftMeasure period)
theorem
EulerH6Nonlinear.transport_wordSobolevNorm_bound
(period : ℝ)
[Fact (0 < period)]
(q n : ℕ)
(b : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain 4)
(e : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain q)
(hb :
∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period b x))
(he :
∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period e x))
(hbL2 :
∀ (j : ℕ) (w : Fin j → Fin 4),
MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w b) 2
(EulerLiftedGradientSpace.liftMeasure period))
(heL2 :
∀ (j : ℕ) (w : Fin j → Fin 4),
MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w e) 2
(EulerLiftedGradientSpace.liftMeasure period))
:
wordSobolevNorm period 6 n (transportField period q b e) ≤ productConstant period q * EulerJetProductBounds.leibnizConvolution (fun (l : ℕ) => wordSobolevNorm period 6 l b)
(fun (l : ℕ) => wordSobolevNorm period 6 (l + 1) e) n
The actual transport source has a single derivative on the transported H⁶ block.
theorem
EulerH6Nonlinear.transport_shifted_weighted_bound
(period : ℝ)
[Fact (0 < period)]
(q N : ℕ)
(ρ : ℝ)
(hρ : 0 < ρ)
(b : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain 4)
(e : EulerLiftedGradientSpace.LiftDomain period → EulerSobolev.Domain q)
(hb :
∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period b x))
(he :
∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period e x))
(hbL2 :
∀ (j : ℕ) (w : Fin j → Fin 4),
MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w b) 2
(EulerLiftedGradientSpace.liftMeasure period))
(heL2 :
∀ (j : ℕ) (w : Fin j → Fin 4),
MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w e) 2
(EulerLiftedGradientSpace.liftMeasure period))
:
∑ n ∈ Finset.range N,
↑(n + 1) * EulerPacketWeights.weight ρ (n + 1) * wordSobolevNorm period 6 n (transportField period q b e) ≤ (2 * productConstant period q * ∑ l ∈ Finset.range (N + 1), EulerPacketWeights.weight ρ l * wordSobolevNorm period 6 l b) * ∑ j ∈ Finset.range (N + 1), ↑j * EulerPacketWeights.weight ρ j * wordSobolevNorm period 6 j e
Source18's transport forcing bound, with every velocity derivative at or below the cutoff N.