A phase-independent L² trace estimate for actual descended tensors. One extra angular derivative suffices, and its norm is controlled by the next actual cover tensor.

theorem EulerCylinderJetGraphTrace.fieldDerivative_descend (P : ℝ) [Fact (0 < P)] {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftTangent → W) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (a : EulerLiftedGradientSpace.LiftTangent) (q : EulerLiftedGradientSpace.LiftDomain P) : EulerTransportDerivatives.fieldDerivative P a (EulerCylinderCoverDescent.descend P f) q = (fderiv ℝ f (EulerCylinderCoverDescent.sectionPoint P q)) a

theorem EulerCylinderJetGraphTrace.jetSeries_smooth (P : ℝ) [Fact (0 < P)] {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftTangent → W) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (q : EulerLiftedGradientSpace.LiftDomain P) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P (fun (x : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f x n) q)

theorem EulerCylinderJetGraphTrace.angularJet_bound (P : ℝ) [Fact (0 < P)] {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftTangent → W) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (n : ℕ) (q : EulerLiftedGradientSpace.LiftDomain P) : ‖EulerTransportDerivatives.fieldDerivative P (0, 1) (fun (x : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f x n) q‖ ≤ ‖EulerCylinderCoverDescent.jetSeries P f q (n + 1)‖

theorem EulerCylinderJetGraphTrace.angularJet_memLp_and_bound (P : ℝ) [Fact (0 < P)] {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftTangent → W) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (hLp : MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q (n + 1)) 2 (EulerLiftedGradientSpace.liftMeasure P)) : MeasureTheory.MemLp (EulerTransportDerivatives.fieldDerivative P (0, 1) fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P) ∧ (MeasureTheory.eLpNorm (EulerTransportDerivatives.fieldDerivative P (0, 1) fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q (n + 1)) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal

theorem EulerCylinderJetGraphTrace.graph_norm_bound (P : ℝ) [Fact (0 < P)] {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] (g : EulerLiftedGradientSpace.LiftDomain P → W) (hg : ∀ (q : EulerLiftedGradientSpace.LiftDomain P), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift P g q)) (hLp : MeasureTheory.MemLp g 2 (EulerLiftedGradientSpace.liftMeasure P)) (hDLp : MeasureTheory.MemLp (EulerTransportDerivatives.fieldDerivative P (0, 1) g) 2 (EulerLiftedGradientSpace.liftMeasure P)) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (C D : ℝ) (hC : 0 ≤ C) (hD : 0 ≤ D) (hn : (MeasureTheory.eLpNorm g 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C) (hd : (MeasureTheory.eLpNorm (EulerTransportDerivatives.fieldDerivative P (0, 1) g) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ D) : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.Vector3) => g (x, θ x)) 2 MeasureTheory.volume ∧ (MeasureTheory.eLpNorm (fun (x : EulerLiftedGradientSpace.Vector3) => g (x, θ x)) 2 MeasureTheory.volume).toReal ≤ √(2 / P + 2 * P) * (C + D)

theorem EulerCylinderJetGraphTrace.jet_graph_memLp_and_bound (P : ℝ) [Fact (0 < P)] {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftTangent → W) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) [CompleteSpace W] (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (hLp : MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hLp₁ : MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q (n + 1)) 2 (EulerLiftedGradientSpace.liftMeasure P)) (θ : EulerLiftedGradientSpace.Vector3 → AddCircle P) (hθ : Continuous θ) (C D : ℝ) (hC : 0 ≤ C) (hD : 0 ≤ D) (hn : (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C) (hd : (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q (n + 1)) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ D) : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.Vector3) => EulerCylinderCoverDescent.jetSeries P f (x, θ x) n) 2 MeasureTheory.volume ∧ (MeasureTheory.eLpNorm (fun (x : EulerLiftedGradientSpace.Vector3) => EulerCylinderCoverDescent.jetSeries P f (x, θ x) n) 2 MeasureTheory.volume).toReal ≤ √(2 / P + 2 * P) * (C + D)