Real-valued forms of the cylinder Sobolev and multiplication estimates.
theorem
EulerRealCylinder.fieldDerivative_postcomp
(period : ℝ)
{F : Type u_1}
{G : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
(L : F →L[ℝ] G)
(a : EulerLiftedGradientSpace.LiftTangent)
(f : EulerLiftedGradientSpace.LiftDomain period → F)
(hf :
∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x))
:
EulerTransportDerivatives.fieldDerivative period a (⇑L ∘ f) = ⇑L ∘ EulerTransportDerivatives.fieldDerivative period a f
theorem
EulerRealCylinder.iteratedFieldDerivative_postcomp
(period : ℝ)
{F : Type u_1}
{G : Type u_2}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
{n : ℕ}
(L : F →L[ℝ] G)
(w : Fin n → Fin 4)
(f : EulerLiftedGradientSpace.LiftDomain period → F)
(hf :
∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x))
:
EulerCylinderSobolev.iteratedFieldDerivative period w (⇑L ∘ f) = ⇑L ∘ EulerCylinderSobolev.iteratedFieldDerivative period w f
noncomputable def
EulerRealCylinder.complexField
(period : ℝ)
(f : EulerLiftedGradientSpace.LiftDomain period → ℝ)
:
EulerLiftedGradientSpace.LiftDomain period → ℂ
Isometric complexification of a real scalar cylinder field.
Equations
- EulerRealCylinder.complexField period f = ⇑Complex.ofRealCLM ∘ f
Instances For
theorem
EulerRealCylinder.complexField_smooth
(period : ℝ)
(f : EulerLiftedGradientSpace.LiftDomain period → ℝ)
(hf :
∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x))
(x : EulerLiftedGradientSpace.LiftDomain period)
:
ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (complexField period f) x)
theorem
EulerRealCylinder.complexField_word
(period : ℝ)
{n : ℕ}
(w : Fin n → Fin 4)
(f : EulerLiftedGradientSpace.LiftDomain period → ℝ)
(hf :
∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x))
:
EulerCylinderSobolev.iteratedFieldDerivative period w (complexField period f) = complexField period (EulerCylinderSobolev.iteratedFieldDerivative period w f)
theorem
EulerRealCylinder.complexField_eLpNorm
(period : ℝ)
[Fact (0 < period)]
(f : EulerLiftedGradientSpace.LiftDomain period → ℝ)
:
MeasureTheory.eLpNorm (complexField period f) 2 (EulerLiftedGradientSpace.liftMeasure period) = MeasureTheory.eLpNorm f 2 (EulerLiftedGradientSpace.liftMeasure period)
theorem
EulerRealCylinder.complexField_memLp
(period : ℝ)
[Fact (0 < period)]
(f : EulerLiftedGradientSpace.LiftDomain period → ℝ)
(hf : MeasureTheory.MemLp f 2 (EulerLiftedGradientSpace.liftMeasure period))
:
MeasureTheory.MemLp (complexField period f) 2 (EulerLiftedGradientSpace.liftMeasure period)
theorem
EulerRealCylinder.complexField_sobolevNorm
(period : ℝ)
[Fact (0 < period)]
(s : ℕ)
(f : EulerLiftedGradientSpace.LiftDomain period → ℝ)
(hf :
∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x))
:
EulerCylinderSobolev.liftSobolevNorm period s (complexField period f) = EulerCylinderSobolev.liftSobolevNorm period s f
theorem
EulerRealCylinder.real_cylinder_pointwise_le_H3
(period : ℝ)
[Fact (0 < period)]
(f : EulerLiftedGradientSpace.LiftDomain period → ℝ)
(hf :
∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x))
(hfL2 :
∀ j ≤ 3,
∀ (w : Fin j → Fin 4),
MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2
(EulerLiftedGradientSpace.liftMeasure period))
(x : EulerLiftedGradientSpace.LiftDomain period)
:
‖f x‖ ≤ EulerCylinderSobolev.cylinderEmbeddingConstant period * EulerCylinderSobolev.liftSobolevNorm period 3 f
The actual real H³ to L∞ embedding on the cylinder.
theorem
EulerRealCylinder.real_cylinder_H6_algebra
(period : ℝ)
[Fact (0 < period)]
(f g : EulerLiftedGradientSpace.LiftDomain period → ℝ)
(hf :
∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x))
(hg :
∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x))
(hfL2 :
∀ j ≤ 6,
∀ (w : Fin j → Fin 4),
MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w f) 2
(EulerLiftedGradientSpace.liftMeasure period))
(hgL2 :
∀ j ≤ 6,
∀ (w : Fin j → Fin 4),
MeasureTheory.MemLp (EulerCylinderSobolev.iteratedFieldDerivative period w g) 2
(EulerLiftedGradientSpace.liftMeasure period))
:
EulerCylinderSobolev.liftSobolevNorm period 6 (f * g) ≤ 5461 * 128 * EulerCylinderAlgebra.lowDerivativeConstant period * EulerCylinderSobolev.liftSobolevNorm period 6 f * EulerCylinderSobolev.liftSobolevNorm period 6 g
The real H⁶ algebra estimate on the actual cylinder.