Periodic cover Gevrey bounds give actual physical graph bounds. The L² trace uses one extra angular derivative but no extra factor of the graph frequency. Only the n physical derivatives cost its n-th power.

noncomputable def EulerCylinderGraphGevrey.graphFactor (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) : ℝ

Graph factor, given by 1+|k| * ‖m‖.

Equations

• EulerCylinderGraphGevrey.graphFactor k m = 1 + |k| * ‖m‖

theorem EulerCylinderGraphGevrey.graphFactor_nonneg (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) : 0 ≤ graphFactor k m

theorem EulerCylinderGraphGevrey.norm_graph_derivative_le {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftTangent → W) (hf : ContDiff ℝ (↑⊤) f) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (n : ℕ) (x : EulerLiftedGradientSpace.Vector3) : ‖iteratedFDeriv ℝ n (f ∘ ⇑(EulerGraphPullback.graphMap k m)) x‖ ≤ graphFactor k m ^ n * ‖iteratedFDeriv ℝ n f ((EulerGraphPullback.graphMap k m) x)‖

theorem EulerCylinderGraphGevrey.graph_sup_bound {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : EulerLiftedGradientSpace.LiftTangent → W) (hf : ContDiff ℝ (↑⊤) f) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (B R : ℝ) (hb : ∀ (n : ℕ) (z : EulerLiftedGradientSpace.LiftTangent), ‖iteratedFDeriv ℝ n f z‖ ≤ B * R ^ n * ↑n.factorial ^ 2) (n : ℕ) (x : EulerLiftedGradientSpace.Vector3) : ‖iteratedFDeriv ℝ n (f ∘ ⇑(EulerGraphPullback.graphMap k m)) x‖ ≤ B * (R * graphFactor k m) ^ n * ↑n.factorial ^ 2

theorem EulerCylinderGraphGevrey.graph_evaluated_tensor_bound {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftTangent → W) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (hf : ContDiff ℝ (↑⊤) f) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hLp : ∀ (n : ℕ), MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hn : ∀ (n : ℕ), (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C * R ^ n * ↑n.factorial ^ 2) (n : ℕ) : MeasureTheory.MemLp (fun (x : EulerLiftedGradientSpace.Vector3) => iteratedFDeriv ℝ n f ((EulerGraphPullback.graphMap k m) x)) 2 MeasureTheory.volume ∧ (MeasureTheory.eLpNorm (fun (x : EulerLiftedGradientSpace.Vector3) => iteratedFDeriv ℝ n f ((EulerGraphPullback.graphMap k m) x)) 2 MeasureTheory.volume).toReal ≤ √(2 / P + 2 * P) * C * (1 + R) * (4 * R) ^ n * ↑n.factorial ^ 2

theorem EulerCylinderGraphGevrey.graph_Lp_bound {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] [CompleteSpace W] (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftTangent → W) (hperiod : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (hf : ContDiff ℝ (↑⊤) f) (k : ℝ) (m : EulerLiftedGradientSpace.Vector3) (C R : ℝ) (hC : 0 ≤ C) (hR : 0 ≤ R) (hLp : ∀ (n : ℕ), MeasureTheory.MemLp (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)) (hn : ∀ (n : ℕ), (MeasureTheory.eLpNorm (fun (q : EulerLiftedGradientSpace.LiftDomain P) => EulerCylinderCoverDescent.jetSeries P f q n) 2 (EulerLiftedGradientSpace.liftMeasure P)).toReal ≤ C * R ^ n * ↑n.factorial ^ 2) (n : ℕ) : MeasureTheory.MemLp (iteratedFDeriv ℝ n (f ∘ ⇑(EulerGraphPullback.graphMap k m))) 2 MeasureTheory.volume ∧ (MeasureTheory.eLpNorm (iteratedFDeriv ℝ n (f ∘ ⇑(EulerGraphPullback.graphMap k m))) 2 MeasureTheory.volume).toReal ≤ √(2 / P + 2 * P) * C * (1 + R) * (4 * R * graphFactor k m) ^ n * ↑n.factorial ^ 2