Bounded linear maps act on the actual descended tensors and their L² classes. In particular the small normal component is retained in the four-dimensional transport estimate.
theorem
EulerCylinderJetLp.tensor_map
(P : ℝ)
[Fact (0 < P)]
{V : Type u_1}
{W : Type u_2}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup W]
[NormedSpace ℝ W]
(L : V →L[ℝ] W)
(f : EulerLiftedGradientSpace.LiftDomain P → V)
(hf : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f q))
(n : ℕ)
(q : EulerLiftedGradientSpace.LiftDomain P)
:
tensor P (fun (x : EulerLiftedGradientSpace.LiftDomain P) => L (f x)) n q = L.compContinuousMultilinearMap (tensor P f n q)
theorem
EulerCylinderJetLp.tensor_map_memLp
(P : ℝ)
[Fact (0 < P)]
{V : Type u_1}
{W : Type u_2}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup W]
[NormedSpace ℝ W]
(L : V →L[ℝ] W)
(f : EulerLiftedGradientSpace.LiftDomain P → V)
(hf : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f q))
(n : ℕ)
(hLp : MeasureTheory.MemLp (tensor P f n) 2 (EulerLiftedGradientSpace.liftMeasure P))
:
MeasureTheory.MemLp (tensor P (fun (x : EulerLiftedGradientSpace.LiftDomain P) => L (f x)) n) 2
(EulerLiftedGradientSpace.liftMeasure P)
theorem
EulerCylinderJetLp.tensor_map_norm_le
(P : ℝ)
[Fact (0 < P)]
{V : Type u_1}
{W : Type u_2}
[NormedAddCommGroup V]
[NormedSpace ℝ V]
[NormedAddCommGroup W]
[NormedSpace ℝ W]
(L : V →L[ℝ] W)
(f : EulerLiftedGradientSpace.LiftDomain P → V)
(hf : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f q))
(n : ℕ)
(hLp : MeasureTheory.MemLp (tensor P f n) 2 (EulerLiftedGradientSpace.liftMeasure P))
:
(MeasureTheory.eLpNorm (tensor P (fun (x : EulerLiftedGradientSpace.LiftDomain P) => L (f x)) n) 2
(EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ ‖L‖ * (MeasureTheory.eLpNorm (tensor P f n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal
theorem
EulerCylinderJetLp.tensor_transport_split
(P : ℝ)
[Fact (0 < P)]
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(f : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3)
(hf : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f q))
(n : ℕ)
(q : EulerLiftedGradientSpace.LiftDomain P)
:
tensor P (fun (x : EulerLiftedGradientSpace.LiftDomain P) => EulerMetricTransport.transportDirection κ m (f x)) n q = κ • tensor P
(fun (x : EulerLiftedGradientSpace.LiftDomain P) =>
(ContinuousLinearMap.inl ℝ EulerLiftedGradientSpace.Vector3 ℝ) (f x))
n q + tensor P
(fun (x : EulerLiftedGradientSpace.LiftDomain P) =>
EulerLiftedSmoothTimeField.angularInjection ((EulerPacketCylinderField.normalComponentMap m) (f x)))
n q
theorem
EulerCylinderJetLp.tensor_transport_norm_le
(P : ℝ)
[Fact (0 < P)]
(κ : ℝ)
(m : EulerLiftedGradientSpace.Vector3)
(f : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3)
(hf : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f q))
(n : ℕ)
(hLp : MeasureTheory.MemLp (tensor P f n) 2 (EulerLiftedGradientSpace.liftMeasure P))
:
(MeasureTheory.eLpNorm
(tensor P (fun (x : EulerLiftedGradientSpace.LiftDomain P) => EulerMetricTransport.transportDirection κ m (f x))
n)
2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ |κ| * (MeasureTheory.eLpNorm (tensor P f n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal + (MeasureTheory.eLpNorm
(tensor P
(fun (x : EulerLiftedGradientSpace.LiftDomain P) => (EulerPacketCylinderField.normalComponentMap m) (f x)) n)
2 (EulerLiftedGradientSpace.liftMeasure P)).toReal