The actual parent deformation supplies inverse and strain bounds with polynomial constants. Determinant one removes any inverse-derivative input.

Polynomial Gevrey bounds for the actual inverse, strain and curvature recovered from a determinant-one deformation and its first two time jets.

@[instance_reducible]

noncomputable def EulerPacketCofactor.instPacketCofactorGevrey1 : NormedAddCommGroup EndSpace

Cache the standard NormedAddCommGroup EndSpace instance to shorten typeclass synthesis.

Equations

• EulerPacketCofactor.instPacketCofactorGevrey1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCofactor.instPacketCofactorGevrey2 : NormedSpace ℝ EndSpace

Cache the standard NormedSpace ℝ EndSpace instance to shorten typeclass synthesis.

Equations

• EulerPacketCofactor.instPacketCofactorGevrey2 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCofactor.instPacketCofactorGevrey3 : NormedAddCommGroup (EndSpace →L[ℝ] EndSpace)

Cache the standard NormedAddCommGroup (EndSpace →L[ℝ] EndSpace) instance to shorten typeclass synthesis.

Equations

• EulerPacketCofactor.instPacketCofactorGevrey3 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCofactor.instPacketCofactorGevrey4 : NormedSpace ℝ (EndSpace →L[ℝ] EndSpace)

Cache the standard NormedSpace ℝ (EndSpace →L[ℝ] EndSpace) instance to shorten typeclass synthesis.

Equations

• EulerPacketCofactor.instPacketCofactorGevrey4 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCofactor.instPacketCofactorGevrey5 : NormedAddCommGroup (EndSpace →L[ℝ] EndSpace →L[ℝ] EndSpace)

Cache the standard NormedAddCommGroup (EndSpace →L[ℝ] EndSpace →L[ℝ] EndSpace) instance to shorten typeclass synthesis.

Equations

• EulerPacketCofactor.instPacketCofactorGevrey5 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCofactor.instPacketCofactorGevrey6 : NormedSpace ℝ (EndSpace →L[ℝ] EndSpace →L[ℝ] EndSpace)

Cache the standard NormedSpace ℝ (EndSpace →L[ℝ] EndSpace →L[ℝ] EndSpace) instance to shorten typeclass synthesis.

Equations

• EulerPacketCofactor.instPacketCofactorGevrey6 = inferInstance

theorem EulerPacketCofactor.adjugate_contDiff {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (F : P → EndSpace) (hF : ContDiff ℝ (↑⊤) F) : ContDiff ℝ ↑⊤ fun (x : P) => adjugate (F x)

theorem EulerPacketCofactor.adjugate_bound {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (F : P → EndSpace) (hF : ContDiff ℝ (↑⊤) F) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hFb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n F x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n (fun (y : P) => adjugate (F y)) x‖ ≤ 9 * C ^ 2 * EulerGevrey.majorant R 0 n

theorem EulerPacketCofactor.inverse_contDiff {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (F I : P → EndSpace) (hF : ContDiff ℝ (↑⊤) F) (hdet : ∀ (x : P), Matrix.det (EulerPacketPiola.operatorMatrix (F x)) = 1) (hI : ∀ (x : P) (v : EulerSmoothLimit.Space), (I x) ((F x) v) = v) : ContDiff ℝ (↑⊤) I

theorem EulerPacketCofactor.inverse_bound {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (F I : P → EndSpace) (hF : ContDiff ℝ (↑⊤) F) (hdet : ∀ (x : P), Matrix.det (EulerPacketPiola.operatorMatrix (F x)) = 1) (hI : ∀ (x : P) (v : EulerSmoothLimit.Space), (I x) ((F x) v) = v) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hFb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n F x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n I x‖ ≤ 9 * C ^ 2 * EulerGevrey.majorant R 0 n

theorem EulerPacketCofactor.recovered_strain_eq {P : Type u_1} (F F₁ M : P → EndSpace) (hdet : ∀ (x : P), Matrix.det (EulerPacketPiola.operatorMatrix (F x)) = 1) (h₁ : ∀ (x : P) (v : EulerSmoothLimit.Space), (F₁ x) v = (M x) ((F x) v)) : M = fun (x : P) => F₁ x ∘SL adjugate (F x)

theorem EulerPacketCofactor.recovered_curvature_eq {P : Type u_1} (F F₂ H : P → EndSpace) (hdet : ∀ (x : P), Matrix.det (EulerPacketPiola.operatorMatrix (F x)) = 1) (h₂ : ∀ (x : P) (v : EulerSmoothLimit.Space), (F₂ x) v = -(H x) ((F x) v)) : H = fun (x : P) => -F₂ x ∘SL adjugate (F x)

theorem EulerPacketCofactor.strain_bound {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (F F₁ M : P → EndSpace) (hF : ContDiff ℝ (↑⊤) F) (hF₁ : ContDiff ℝ (↑⊤) F₁) (hdet : ∀ (x : P), Matrix.det (EulerPacketPiola.operatorMatrix (F x)) = 1) (h₁ : ∀ (x : P) (v : EulerSmoothLimit.Space), (F₁ x) v = (M x) ((F x) v)) (R C C₁ : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hFb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n F x‖ ≤ C * EulerGevrey.majorant R 0 n) (hF₁b : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n F₁ x‖ ≤ C₁ * EulerGevrey.majorant R 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n M x‖ ≤ 27 * C ^ 2 * C₁ * EulerGevrey.majorant R 0 n

theorem EulerPacketCofactor.curvature_bound {P : Type u_1} [NormedAddCommGroup P] [NormedSpace ℝ P] (F F₂ H : P → EndSpace) (hF : ContDiff ℝ (↑⊤) F) (hF₂ : ContDiff ℝ (↑⊤) F₂) (hdet : ∀ (x : P), Matrix.det (EulerPacketPiola.operatorMatrix (F x)) = 1) (h₂ : ∀ (x : P) (v : EulerSmoothLimit.Space), (F₂ x) v = -(H x) ((F x) v)) (R C C₂ : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₂ : 0 ≤ C₂) (hFb : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n F x‖ ≤ C * EulerGevrey.majorant R 0 n) (hF₂b : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n F₂ x‖ ≤ C₂ * EulerGevrey.majorant R 0 n) (n : ℕ) (x : P) : ‖iteratedFDeriv ℝ n H x‖ ≤ 27 * C ^ 2 * C₂ * EulerGevrey.majorant R 0 n

@[instance_reducible]

noncomputable def EulerPacketCofactor.instPacketParentCoefficientBounds1 : NormedAddCommGroup EndSpace

Cache the standard NormedAddCommGroup EndSpace instance to shorten typeclass synthesis.

Equations

• EulerPacketCofactor.instPacketParentCoefficientBounds1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCofactor.instPacketParentCoefficientBounds2 : NormedSpace ℝ EndSpace

Cache the standard NormedSpace ℝ EndSpace instance to shorten typeclass synthesis.

Equations

• EulerPacketCofactor.instPacketParentCoefficientBounds2 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCofactor.instPacketParentCoefficientBounds3 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space EndSpace)

Cache the standard NormedAddCommGroup (Space →ᵇ EndSpace) instance to shorten typeclass synthesis.

Equations

• EulerPacketCofactor.instPacketParentCoefficientBounds3 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCofactor.instPacketParentCoefficientBounds4 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space EndSpace)

Cache the standard NormedSpace ℝ (Space →ᵇ EndSpace) instance to shorten typeclass synthesis.

Equations

• EulerPacketCofactor.instPacketParentCoefficientBounds4 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCofactor.instPacketParentCoefficientBounds5 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, BoundedContinuousFunction EulerSmoothLimit.Space EndSpace)

Cache the standard NormedAddCommGroup C(K,Space →ᵇ EndSpace) instance to shorten typeclass synthesis.

Equations

• EulerPacketCofactor.instPacketParentCoefficientBounds5 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketCofactor.instPacketParentCoefficientBounds6 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, BoundedContinuousFunction EulerSmoothLimit.Space EndSpace)

Cache the standard NormedSpace ℝ C(K,Space →ᵇ EndSpace) instance to shorten typeclass synthesis.

Equations

• EulerPacketCofactor.instPacketParentCoefficientBounds6 = inferInstance

theorem EulerPacketCofactor.coefficientPath_norm_le {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (F : EulerMeanCoefficients.SmoothCoefficientPath K EndSpace) (C : ℝ) (hC : 0 ≤ C) (hF : ∀ (t : K) (x : EulerSmoothLimit.Space), ‖(F.field t) x‖ ≤ C) : ‖F.field‖ ≤ C

theorem EulerPacketCofactor.coefficientPath_norm_le_of_gevrey {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (F : EulerMeanCoefficients.SmoothCoefficientPath K EndSpace) (R C : ℝ) (hC : 0 ≤ C) (hF : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) : ‖F.field‖ ≤ C

theorem EulerPacketCofactor.coefficientInverse_norm_le {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (F : EulerMeanCoefficients.SmoothCoefficientPath K EndSpace) (I : C(K, BoundedContinuousFunction EulerSmoothLimit.Space EndSpace)) (hdet : ∀ (t : K) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((F.field t) x)) = 1) (hI : ∀ (t : K) (x v : EulerSmoothLimit.Space), ((I t) x) (((F.field t) x) v) = v) (C : ℝ) (_hC : 0 ≤ C) (hF : ∀ (t : K) (x : EulerSmoothLimit.Space), ‖(F.field t) x‖ ≤ C) : ‖I‖ ≤ 3 * C ^ 2

theorem EulerPacketCofactor.coefficientInverse_bound {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (F : EulerMeanCoefficients.SmoothCoefficientPath K EndSpace) (I : C(K, BoundedContinuousFunction EulerSmoothLimit.Space EndSpace)) (hdet : ∀ (t : K) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((F.field t) x)) = 1) (hI : ∀ (t : K) (x v : EulerSmoothLimit.Space), ((I t) x) (((F.field t) x) v) = v) (R C : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hF : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (n : ℕ) (t : K) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(I t)) x‖ ≤ 9 * C ^ 2 * EulerGevrey.majorant R 0 n

theorem EulerPacketCofactor.coefficientStrain_bound {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (F F₁ M : EulerMeanCoefficients.SmoothCoefficientPath K EndSpace) (hdet : ∀ (t : K) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((F.field t) x)) = 1) (h₁ : ∀ (t : K) (x v : EulerSmoothLimit.Space), ((F₁.field t) x) v = ((M.field t) x) (((F.field t) x) v)) (R C C₁ : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hF : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (hF₁ : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F₁.field t)) x‖ ≤ C₁ * EulerGevrey.majorant R 0 n) (n : ℕ) (t : K) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(M.field t)) x‖ ≤ 27 * C ^ 2 * C₁ * EulerGevrey.majorant R 0 n

theorem EulerPacketCofactor.coefficientCurvature_bound {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (F F₂ H : EulerMeanCoefficients.SmoothCoefficientPath K EndSpace) (hdet : ∀ (t : K) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((F.field t) x)) = 1) (h₂ : ∀ (t : K) (x v : EulerSmoothLimit.Space), ((F₂.field t) x) v = -((H.field t) x) (((F.field t) x) v)) (R C C₂ : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₂ : 0 ≤ C₂) (hF : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F.field t)) x‖ ≤ C * EulerGevrey.majorant R 0 n) (hF₂ : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(F₂.field t)) x‖ ≤ C₂ * EulerGevrey.majorant R 0 n) (n : ℕ) (t : K) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(H.field t)) x‖ ≤ 27 * C ^ 2 * C₂ * EulerGevrey.majorant R 0 n

theorem EulerTransversePacketProvider.Data.inverseBound_le_of_frame {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (C : ℝ) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖(D.F.field t) x‖ ≤ C) : D.inverseBound ≤ 1 + 3 * C ^ 2

theorem EulerTransversePacketProvider.Data.frameBound_le_of_frame {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (C : ℝ) (hC : 0 ≤ C) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖(D.F.field t) x‖ ≤ C) : D.frameBound ≤ 1 + C

theorem EulerTransversePacketProvider.Data.frameLower_inv_le_of_frame {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (C : ℝ) (hC : 0 ≤ C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖(D.F.field t) x‖ ≤ C) : D.frameLower⁻¹ ≤ (1 + 3 * C ^ 2) ^ 2

theorem EulerTransversePacketProvider.Data.normalLower_inv_le_of_frame {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (C : ℝ) (hC : 0 ≤ C) (hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖(D.F.field t) x‖ ≤ C) : D.normalLower⁻¹ ≤ (1 + C) ^ 2