Keeping the physical label scale in the coefficient bounds gives one factor ell for each normalized spatial derivative. This factor is needed in the neighboring-label estimates of the induction.

theorem EulerOperatorGevreyCalculus.scalar_precomp_bound {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] (f : E → V) (hf : ContDiff ℝ (↑⊤) f) (C R ell : ℝ) (hell : 0 ≤ ell) (hb : ∀ (n : ℕ) (x : E), ‖iteratedFDeriv ℝ n f x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) (x : E) : ‖iteratedFDeriv ℝ n (fun (y : E) => f (ell • y)) x‖ ≤ C * EulerGevrey.majorant (ell * R) 0 n

def EulerParentPacketFrames.LabelData.scaledRadius {G : Parent} (L : LabelData G) : ℝ

Scaled radius, given by G.ell*coefficientRadius L.K.

Equations

• L.scaledRadius = G.ell * EulerPacketParentLabelBounds.coefficientRadius L.K

theorem EulerParentPacketFrames.LabelData.scaledRadius_nonneg {G : Parent} (L : LabelData G) : 0 ≤ L.scaledRadius

theorem EulerParentPacketFrames.LabelData.scaled_gradient_bound {G : Parent} (L : LabelData G) (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hA : EulerPacketParentLabelBounds.HasLabelBound L.K A) (n : ℕ) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (y : EulerSmoothLimit.Space) => fderiv ℝ A.field (G.ell • y)) x‖ ≤ EulerPacketParentLabelBounds.gradientAmplitude L.K * EulerGevrey.majorant L.scaledRadius 0 n

theorem EulerParentPacketFrames.LabelData.frame_scaled_bound {G : Parent} (L : LabelData G) (n : ℕ) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(G.frame.field t)) x‖ ≤ EulerPacketParentLabelBounds.frameAmplitude L.K * EulerGevrey.majorant L.scaledRadius 0 n

theorem EulerParentPacketFrames.LabelData.first_scaled_bound {G : Parent} (L : LabelData G) (n : ℕ) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(G.first.field t)) x‖ ≤ EulerPacketParentLabelBounds.gradientAmplitude L.K * EulerGevrey.majorant L.scaledRadius 0 n

theorem EulerParentPacketFrames.LabelData.second_scaled_bound {G : Parent} (L : LabelData G) (n : ℕ) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(G.second.field t)) x‖ ≤ EulerPacketParentLabelBounds.gradientAmplitude L.K * EulerGevrey.majorant L.scaledRadius 0 n

theorem EulerParentPacketFrames.LabelData.inverse_scaled_bound {G : Parent} (L : LabelData G) (n : ℕ) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(G.inverse.field t)) x‖ ≤ 9 * EulerPacketParentLabelBounds.frameAmplitude L.K ^ 2 * EulerGevrey.majorant L.scaledRadius 0 n

theorem EulerParentPacketFrames.LabelData.strain_scaled_bound {G : Parent} (L : LabelData G) (n : ℕ) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(G.strain.field t)) x‖ ≤ 27 * EulerPacketParentLabelBounds.frameAmplitude L.K ^ 2 * EulerPacketParentLabelBounds.gradientAmplitude L.K * EulerGevrey.majorant L.scaledRadius 0 n

theorem EulerParentPacketFrames.LabelData.curvature_scaled_bound {G : Parent} (L : LabelData G) (n : ℕ) (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(G.curvature.field t)) x‖ ≤ 27 * EulerPacketParentLabelBounds.frameAmplitude L.K ^ 2 * EulerPacketParentLabelBounds.gradientAmplitude L.K * EulerGevrey.majorant L.scaledRadius 0 n