The actual inverse parent flow preserves source Gevrey regularity

The inverse derivative bounds are derived from the prescribed deformation and its determinant-one cofactor identity. Neither inverse-flow jets nor inverse-deformation jets are independent assumptions.

theorem EulerPacketInverseFlowGevrey.inverseFlow_fderiv {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hY : ∀ (t : ↑(Set.Icc 0 D.T)), Differentiable ℝ (Y t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : fderiv ℝ (Y t) x = (D.FInv.field t) (Y t x)

theorem EulerPacketInverseFlowGevrey.inverseFlow_contDiff {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hY : ∀ (t : ↑(Set.Icc 0 D.T)), Differentiable ℝ (Y t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (t : ↑(Set.Icc 0 D.T)) : ContDiff ℝ (↑⊤) (Y t)

def EulerPacketInverseFlowGevrey.sourceInverseRadius (C R : ℝ) : ℝ

Source inverse radius, given by 1 + 18*C^2*R.

Equations

• EulerPacketInverseFlowGevrey.sourceInverseRadius C R = 1 + 18 * C ^ 2 * R

theorem EulerPacketInverseFlowGevrey.sourceInverseRadius_eq (C R : ℝ) : sourceInverseRadius C R = EulerGevreyComposition.inverseMapRadius (9 * C ^ 2) R

theorem EulerPacketInverseFlowGevrey.sourceInverseRadius_pos (C R : ℝ) (hR : 0 ≤ R) : 0 < sourceInverseRadius C R

theorem EulerPacketInverseFlowGevrey.inverseFlow_gevrey {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hY : ∀ (t : ↑(Set.Icc 0 D.T)), Differentiable ℝ (Y t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ (n + 1) (Y t) x‖ ≤ 9 * C ^ 2 * sourceInverseRadius C R ^ n * ↑n.factorial ^ 2

theorem EulerPacketInverseFlowGevrey.pullback_gevrey {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hY : ∀ (t : ↑(Set.Icc 0 D.T)), Differentiable ℝ (Y t)) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] (g : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → V) (hg : ∀ (t : ↑(Set.Icc 0 D.T)), ContDiff ℝ (↑⊤) (g t)) (A S : ℝ) (hA : 0 ≤ A) (hS : 0 ≤ S) (hgjet : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (g t) x‖ ≤ A * S ^ n * ↑n.factorial ^ 2) (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (fun (y : EulerSmoothLimit.Space) => g t (Y t y)) x‖ ≤ A * (sourceInverseRadius C R * (9 * C ^ 2 * S + 2)) ^ n * ↑n.factorial ^ 2

The coordinate change in the physical packet only changes the fixed Gevrey radius; the small correction amplitude is retained exactly.