Related estimates used together by the same construction modules.

Actual cylinder L² tensor bounds from the finite packet's ordered-word budgets. The single coordinate conversion affects only the input radius.

theorem EulerPacketCylinderField.Field.WordBound.coverTensor_bound {P T : ℝ} [Fact (0 < P)] {raw : EulerPacketProfileRecursion.VectorField} {G : Field P T raw} {q : ℕ} {R A : ℝ} (hG : G.WordBound q R A 0) (n : ℕ) (t : ↑(Set.Icc 0 T)) : (MeasureTheory.eLpNorm (EulerCylinderJetLp.tensor P (G.toFieldTower.pointField t) n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ A * (‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * R) ^ n * ↑n.factorial ^ 2

Addition and transport of the actual cylinder derivative tensors. All norm statements concern genuine L² functions on the cylinder.

@[instance_reducible]

noncomputable def EulerCylinderJetLp.instCylinderJetLpAlgebra1 {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedAddCommGroup (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] V)

Cache the standard NormedAddCommGroup (LiftTangent [×n]→L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerCylinderJetLp.instCylinderJetLpAlgebra1 n = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderJetLp.instCylinderJetLpAlgebra2 {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (n : ℕ) : NormedSpace ℝ (EulerLiftedGradientSpace.LiftTangent [×n]→L[ℝ] V)

Cache the standard NormedSpace ℝ (LiftTangent [×n]→L[ℝ] V) instance to shorten typeclass synthesis.

Equations

• EulerCylinderJetLp.instCylinderJetLpAlgebra2 n = inferInstance

theorem EulerCylinderJetLp.tensor_add (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f g : EulerLiftedGradientSpace.LiftDomain P → V) (hf : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f q)) (hg : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P g q)) (n : ℕ) (q : EulerLiftedGradientSpace.LiftDomain P) : tensor P (fun (x : EulerLiftedGradientSpace.LiftDomain P) => f x + g x) n q = tensor P f n q + tensor P g n q

theorem EulerCylinderJetLp.tensor_add_memLp (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f g : EulerLiftedGradientSpace.LiftDomain P → V) (hf : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f q)) (hg : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P g q)) (n : ℕ) (hF : MeasureTheory.MemLp (tensor P f n) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hG : MeasureTheory.MemLp (tensor P g n) 2 (EulerLiftedGradientSpace.liftMeasure P)) : MeasureTheory.MemLp (tensor P (fun (x : EulerLiftedGradientSpace.LiftDomain P) => f x + g x) n) 2 (EulerLiftedGradientSpace.liftMeasure P)

theorem EulerCylinderJetLp.tensor_add_norm_le (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f g : EulerLiftedGradientSpace.LiftDomain P → V) (hf : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f q)) (hg : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P g q)) (n : ℕ) (hF : MeasureTheory.MemLp (tensor P f n) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hG : MeasureTheory.MemLp (tensor P g n) 2 (EulerLiftedGradientSpace.liftMeasure P)) : (MeasureTheory.eLpNorm (tensor P (fun (x : EulerLiftedGradientSpace.LiftDomain P) => f x + g x) n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ (MeasureTheory.eLpNorm (tensor P f n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal + (MeasureTheory.eLpNorm (tensor P g n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal

theorem EulerCylinderJetLp.tensor_transport_norm_le_full (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 : ℕ) (hF : 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 ≤ (|κ| + ‖m‖) * (MeasureTheory.eLpNorm (tensor P f n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal

theorem EulerCylinderJetLp.tensor_transport_add_norm_le (P : ℝ) [Fact (0 < P)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (f g : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.Vector3) (hf : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P f q)) (hg : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P g q)) (n : ℕ) (hF : MeasureTheory.MemLp (tensor P f n) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hG : MeasureTheory.MemLp (tensor P g n) 2 (EulerLiftedGradientSpace.liftMeasure P)) : (MeasureTheory.eLpNorm (tensor P (fun (x : EulerLiftedGradientSpace.LiftDomain P) => EulerMetricTransport.transportDirection κ m (f x + g 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 + (|κ| + ‖m‖) * (MeasureTheory.eLpNorm (tensor P g n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal