Time identities derived from the source deformation data, including the actual inverse and normal paths.

The actual time coefficient of the vector potential, with uniform factorial bounds.

The vector-potential multiplier is a fixed linear contraction of the normal functional.

noncomputable def EulerPacketCrossProduct.normalVector : (EulerSmoothLimit.Space →L[ℝ] ℝ) →L[ℝ] EulerSmoothLimit.Space

Normal vector, given by (ContinuousLinearMap.apply ℝ Space (1 : ℝ)).comp (realAdjoint (U := Space) (E := ℝ)).

Equations

• EulerPacketCrossProduct.normalVector = (ContinuousLinearMap.apply ℝ EulerSmoothLimit.Space) 1 ∘SL EulerTransverseGramInverse.realAdjoint

@[simp]

theorem EulerPacketCrossProduct.normalVector_apply (N : EulerSmoothLimit.Space →L[ℝ] ℝ) : normalVector N = (ContinuousLinearMap.adjoint N) 1

noncomputable def EulerPacketCrossProduct.normalPotentialMap : (EulerSmoothLimit.Space →L[ℝ] ℝ) →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Normal potential map, given by -(crossOperator.comp normalVector).

Equations

• EulerPacketCrossProduct.normalPotentialMap = -EulerPacketCrossProduct.crossOperator ∘SL EulerPacketCrossProduct.normalVector

@[simp]

theorem EulerPacketCrossProduct.normalPotentialMap_apply (N : EulerSmoothLimit.Space →L[ℝ] ℝ) : normalPotentialMap N = -crossLeft ((ContinuousLinearMap.adjoint N) 1)

theorem EulerPacketCrossProduct.normalPotentialMap_norm : ‖normalPotentialMap‖ ≤ 1

theorem EulerPacketCrossProduct.normalVector_eq (m : EulerSmoothLimit.Space) (N : EulerSmoothLimit.Space →L[ℝ] ℝ) (hN : ∀ (v : EulerSmoothLimit.Space), N v = inner ℝ m v / ‖m‖ ^ 2) : (ContinuousLinearMap.adjoint N) 1 = (‖m‖ ^ 2)⁻¹ • m

theorem EulerPacketCrossProduct.normalPotentialMap_eq (m : EulerSmoothLimit.Space) (N : EulerSmoothLimit.Space →L[ℝ] ℝ) (hN : ∀ (v : EulerSmoothLimit.Space), N v = inner ℝ m v / ‖m‖ ^ 2) : normalPotentialMap N = potentialMultiplier m

No additional inverse or derivative estimate is needed after constructing the normal functional.

The literal vector-potential multiplier inherits the source normal coefficient bounds.

@[reducible, inline]

abbrev EulerSourcePotentialCoefficient.NormalField : Type

Normal field: an abbreviation for Space →ᵇ (Space →L[ℝ] ℝ).

Equations

• EulerSourcePotentialCoefficient.NormalField = BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] ℝ)

@[reducible, inline]

abbrev EulerSourcePotentialCoefficient.PotentialField : Type

Potential field: an abbreviation for Space →ᵇ (Space →L[ℝ] Space).

Equations

• EulerSourcePotentialCoefficient.PotentialField = BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialCoefficient1 : NormedAddCommGroup NormalField

Cache the standard NormedAddCommGroup NormalField instance to shorten typeclass synthesis.

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialCoefficient1 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialCoefficient2 : NormedSpace ℝ NormalField

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

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialCoefficient2 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialCoefficient3 : NormedAddCommGroup PotentialField

Cache the standard NormedAddCommGroup PotentialField instance to shorten typeclass synthesis.

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialCoefficient3 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialCoefficient4 : NormedSpace ℝ PotentialField

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

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialCoefficient4 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialCoefficient5 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, NormalField)

Cache the standard NormedAddCommGroup C(K,NormalField) instance to shorten typeclass synthesis.

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialCoefficient5 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialCoefficient6 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, NormalField)

Cache the standard NormedSpace ℝ C(K,NormalField) instance to shorten typeclass synthesis.

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialCoefficient6 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialCoefficient7 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, PotentialField)

Cache the standard NormedAddCommGroup C(K,PotentialField) instance to shorten typeclass synthesis.

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialCoefficient7 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialCoefficient8 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, PotentialField)

Cache the standard NormedSpace ℝ C(K,PotentialField) instance to shorten typeclass synthesis.

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialCoefficient8 = inferInstance

noncomputable def EulerSourcePotentialCoefficient.potentialPathMap {K : Type u_1} [TopologicalSpace K] : C(K, NormalField) →L[ℝ] C(K, PotentialField)

Potential path map, given by (normalPotentialMap.compLeftContinuousBounded Space).compLeftContinuous ℝ K.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem EulerSourcePotentialCoefficient.potentialPathMap_apply {K : Type u_1} [TopologicalSpace K] (N : C(K, NormalField)) (t : K) (x : EulerSmoothLimit.Space) : ((potentialPathMap N) t) x = EulerPacketCrossProduct.normalPotentialMap ((N t) x)

theorem EulerSourcePotentialCoefficient.potentialPathMap_norm {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : ‖potentialPathMap‖ ≤ 1

noncomputable def EulerSourcePotentialCoefficient.potentialCoefficient {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (m : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (x : EulerSmoothLimit.Space), c ≤ ‖(m.field t) x‖ ^ 2) : C(K, PotentialField)

Potential coefficient, given by potentialPathMap (normalFunctional m c hc hm).

Equations

• EulerSourcePotentialCoefficient.potentialCoefficient m c hc hm = EulerSourcePotentialCoefficient.potentialPathMap (EulerSourceNormalCoefficient.normalFunctional m c hc hm)

theorem EulerSourcePotentialCoefficient.potentialCoefficient_apply {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (m : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (x : EulerSmoothLimit.Space), c ≤ ‖(m.field t) x‖ ^ 2) (t : K) (x : EulerSmoothLimit.Space) : ((potentialCoefficient m c hc hm) t) x = EulerPacketCrossProduct.potentialMultiplier ((m.field t) x)

theorem EulerSourcePotentialCoefficient.potentialCoefficient_translated {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (m : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (x : EulerSmoothLimit.Space), c ≤ ‖(m.field t) x‖ ^ 2) (a : EulerSmoothLimit.Space) : EulerMeanCoefficients.translateCoefficientPath (potentialCoefficient m c hc hm) a = potentialPathMap (EulerMeanCoefficients.translateCoefficientPath (EulerSourceNormalCoefficient.normalFunctional m c hc hm) a)

theorem EulerSourcePotentialCoefficient.potentialCoefficient_translation_contDiff {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (m : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (x : EulerSmoothLimit.Space), c ≤ ‖(m.field t) x‖ ^ 2) : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath (potentialCoefficient m c hc hm))

theorem EulerSourcePotentialCoefficient.potentialCoefficient_translation_bound {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (m : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (x : EulerSmoothLimit.Space), c ≤ ‖(m.field t) x‖ ^ 2) (Rc C Ri : ℝ) (hRc : 0 ≤ Rc) (hC : 0 ≤ C) (hRi : 2 * EulerTimeLpGramGevrey.gramCost c C 1 * (Rc + 1) ≤ Ri) (hbm : ∀ (n : ℕ) (t : K) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(m.field t)) x‖ ≤ C * EulerGevrey.majorant Rc 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (potentialCoefficient m c hc hm)) a‖ ≤ 3 * Ri * C * EulerGevrey.majorant (4 * Ri) 0 n

The source coefficient passes through a linear contraction, with no radius or shift change.

An inverse-free polynomial formula for the actual normal multiplier's time derivative.

noncomputable def EulerPacketCrossProduct.normalTimeMap (N : EulerSmoothLimit.Space →L[ℝ] ℝ) (Q₁ : ℝ →L[ℝ] EulerSmoothLimit.Space) : EulerSmoothLimit.Space →L[ℝ] ℝ

Differentiate the normal functional using only itself and the normal's derivative column.

Equations

• EulerPacketCrossProduct.normalTimeMap N Q₁ = (N ∘SL ContinuousLinearMap.adjoint N) ∘SL ContinuousLinearMap.adjoint Q₁ - 2 • (N ∘SL Q₁) ∘SL N

theorem EulerPacketCrossProduct.normalTimeMap_apply (m mt : EulerSmoothLimit.Space) (N : EulerSmoothLimit.Space →L[ℝ] ℝ) (hm : m ≠ 0) (hN : ∀ (v : EulerSmoothLimit.Space), N v = inner ℝ m v / ‖m‖ ^ 2) (v : EulerSmoothLimit.Space) : (normalTimeMap N (ContinuousLinearMap.toSpanSingleton ℝ mt)) v = inner ℝ mt v / ‖m‖ ^ 2 - 2 * inner ℝ m mt / (‖m‖ ^ 2) ^ 2 * inner ℝ m v

theorem EulerPacketCrossProduct.normalTimeMap_vector (m mt : EulerSmoothLimit.Space) (N : EulerSmoothLimit.Space →L[ℝ] ℝ) (hm : m ≠ 0) (hN : ∀ (v : EulerSmoothLimit.Space), N v = inner ℝ m v / ‖m‖ ^ 2) : (ContinuousLinearMap.adjoint (normalTimeMap N (ContinuousLinearMap.toSpanSingleton ℝ mt))) 1 = (‖m‖ ^ 2)⁻¹ • mt - (2 * inner ℝ m mt / (‖m‖ ^ 2) ^ 2) • m

theorem EulerPacketCrossProduct.normalTimeMap_potential (m mt : EulerSmoothLimit.Space) (N : EulerSmoothLimit.Space →L[ℝ] ℝ) (hm : m ≠ 0) (hN : ∀ (v : EulerSmoothLimit.Space), N v = inner ℝ m v / ‖m‖ ^ 2) : normalPotentialMap (normalTimeMap N (ContinuousLinearMap.toSpanSingleton ℝ mt)) = potentialMultiplierDerivative m mt

This polynomial coefficient is exactly the derivative of −cross(m)/|m|².

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] ℝ)

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

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient1 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] ℝ)

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

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient2 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient3 : NormedAddCommGroup (ℝ →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient3 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient4 : NormedSpace ℝ (ℝ →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient4 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient5 : NormedAddCommGroup NormalField

Cache the standard NormedAddCommGroup NormalField instance to shorten typeclass synthesis.

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient5 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient6 : NormedSpace ℝ NormalField

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

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient6 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient7 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (ℝ →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient7 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient8 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (ℝ →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient8 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient9 : NormedAddCommGroup (ℝ →L[ℝ] ℝ)

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

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient9 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient10 : NormedSpace ℝ (ℝ →L[ℝ] ℝ)

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

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient10 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient11 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (ℝ →L[ℝ] ℝ))

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

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient11 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient12 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (ℝ →L[ℝ] ℝ))

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

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient12 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient13 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, NormalField)

Cache the standard NormedAddCommGroup C(K,NormalField) instance to shorten typeclass synthesis.

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient13 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient14 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, NormalField)

Cache the standard NormedSpace ℝ C(K,NormalField) instance to shorten typeclass synthesis.

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient14 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient15 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, BoundedContinuousFunction EulerSmoothLimit.Space (ℝ →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup C(K,Space →ᵇ ℝ →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient15 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient16 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, BoundedContinuousFunction EulerSmoothLimit.Space (ℝ →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient16 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient17 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, BoundedContinuousFunction EulerSmoothLimit.Space (ℝ →L[ℝ] ℝ))

Cache the standard NormedAddCommGroup C(K,Space →ᵇ ℝ →L[ℝ] ℝ) instance to shorten typeclass synthesis.

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient17 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient18 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, BoundedContinuousFunction EulerSmoothLimit.Space (ℝ →L[ℝ] ℝ))

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

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient18 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient19 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient19 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient20 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient20 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient21 : NormedAddCommGroup PotentialField

Cache the standard NormedAddCommGroup PotentialField instance to shorten typeclass synthesis.

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient21 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient22 : NormedSpace ℝ PotentialField

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

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient22 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient23 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, PotentialField)

Cache the standard NormedAddCommGroup C(K,PotentialField) instance to shorten typeclass synthesis.

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient23 = inferInstance

@[instance_reducible]

noncomputable def EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient24 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, PotentialField)

Cache the standard NormedSpace ℝ C(K,PotentialField) instance to shorten typeclass synthesis.

Equations

• EulerSourcePotentialCoefficient.instSourcePotentialTimeCoefficient24 = inferInstance

noncomputable def EulerSourcePotentialCoefficient.timeNormalPath {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (N : C(K, NormalField)) (Q₁ : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (ℝ →L[ℝ] EulerSmoothLimit.Space))) : C(K, NormalField)

Time normal path, constructed using pathCompositionMap.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerSourcePotentialCoefficient.timeNormalPath_apply {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (N : C(K, NormalField)) (Q₁ : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (ℝ →L[ℝ] EulerSmoothLimit.Space))) (t : K) (y : EulerSmoothLimit.Space) : ((timeNormalPath N Q₁) t) y = EulerPacketCrossProduct.normalTimeMap ((N t) y) ((Q₁ t) y)

theorem EulerSourcePotentialCoefficient.timeNormalPath_translation {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (N : C(K, NormalField)) (Q₁ : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (ℝ →L[ℝ] EulerSmoothLimit.Space))) (a : EulerSmoothLimit.Space) : EulerMeanCoefficients.translateCoefficientPath (timeNormalPath N Q₁) a = timeNormalPath (EulerMeanCoefficients.translateCoefficientPath N a) (EulerMeanCoefficients.translateCoefficientPath Q₁ a)

theorem EulerSourcePotentialCoefficient.timeNormalPath_contDiff {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] (N : X → C(K, NormalField)) (Q₁ : X → C(K, BoundedContinuousFunction EulerSmoothLimit.Space (ℝ →L[ℝ] EulerSmoothLimit.Space))) (hN : ContDiff ℝ (↑⊤) N) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) : ContDiff ℝ ↑⊤ fun (a : X) => timeNormalPath (N a) (Q₁ a)

theorem EulerSourcePotentialCoefficient.timeNormalPath_bound {K : Type u_1} [TopologicalSpace K] [CompactSpace K] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] (N : X → C(K, NormalField)) (Q₁ : X → C(K, BoundedContinuousFunction EulerSmoothLimit.Space (ℝ →L[ℝ] EulerSmoothLimit.Space))) (hN : ContDiff ℝ (↑⊤) N) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (R C D : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hD : 0 ≤ D) (hbN : ∀ (n : ℕ) (a : X), ‖iteratedFDeriv ℝ n N a‖ ≤ C * EulerGevrey.majorant R 0 n) (hbQ₁ : ∀ (n : ℕ) (a : X), ‖iteratedFDeriv ℝ n Q₁ a‖ ≤ D * EulerGevrey.majorant R 0 n) (n : ℕ) (a : X) : ‖iteratedFDeriv ℝ n (fun (x : X) => timeNormalPath (N x) (Q₁ x)) a‖ ≤ 27 * C ^ 2 * D * EulerGevrey.majorant R 0 n

noncomputable def EulerSourcePotentialCoefficient.potentialTimeCoefficient {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (m m₁ : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (y : EulerSmoothLimit.Space), c ≤ ‖(m.field t) y‖ ^ 2) : C(K, PotentialField)

Potential time coefficient, given by potentialPathMap (timeNormalPath (normalFunctional m c hc hm) (normalColumn m₁).field).

Equations

• One or more equations did not get rendered due to their size.

theorem EulerSourcePotentialCoefficient.potentialTimeCoefficient_apply {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (m m₁ : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (y : EulerSmoothLimit.Space), c ≤ ‖(m.field t) y‖ ^ 2) (t : K) (y : EulerSmoothLimit.Space) : ((potentialTimeCoefficient m m₁ c hc hm) t) y = EulerPacketCrossProduct.potentialMultiplierDerivative ((m.field t) y) ((m₁.field t) y)

theorem EulerSourcePotentialCoefficient.potentialTimeCoefficient_translation {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (m m₁ : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (y : EulerSmoothLimit.Space), c ≤ ‖(m.field t) y‖ ^ 2) : EulerMeanCoefficients.translateCoefficientPath (potentialTimeCoefficient m m₁ c hc hm) = fun (a : EulerSmoothLimit.Space) => potentialPathMap (timeNormalPath (EulerMeanCoefficients.translateCoefficientPath (EulerSourceNormalCoefficient.normalFunctional m c hc hm) a) (EulerMeanCoefficients.translateCoefficientPath (EulerSourceNormalCoefficient.normalColumn m₁).field a))

theorem EulerSourcePotentialCoefficient.potentialTimeCoefficient_translation_contDiff {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (m m₁ : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (y : EulerSmoothLimit.Space), c ≤ ‖(m.field t) y‖ ^ 2) : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath (potentialTimeCoefficient m m₁ c hc hm))

theorem EulerSourcePotentialCoefficient.potentialTimeCoefficient_translation_bound {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (m m₁ : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (y : EulerSmoothLimit.Space), c ≤ ‖(m.field t) y‖ ^ 2) (R C D : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hD : 0 ≤ D) (hbN : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (EulerSourceNormalCoefficient.normalFunctional m c hc hm)) a‖ ≤ C * EulerGevrey.majorant R 0 n) (hbm₁ : ∀ (n : ℕ) (t : K) (y : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(m₁.field t)) y‖ ≤ D * EulerGevrey.majorant R 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (potentialTimeCoefficient m m₁ c hc hm)) a‖ ≤ 27 * C ^ 2 * D * EulerGevrey.majorant R 0 n

The derivative coefficient is polynomial in the already constructed normal functional.

The potential time coefficient from an actual continuous, translation-smooth normal derivative path.

noncomputable def EulerSourcePotentialCoefficient.columnPath {K : Type u_1} [TopologicalSpace K] : C(K, BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space) →L[ℝ] C(K, BoundedContinuousFunction EulerSmoothLimit.Space (ℝ →L[ℝ] EulerSmoothLimit.Space))

Column path, given by mapCoefficientPath (ContinuousLinearMap.toSpanSingletonLIE ℝ Space).toLinearIsometry.toContinuousLinearMap.

Equations

• EulerSourcePotentialCoefficient.columnPath = EulerMeanCoefficients.mapCoefficientPath (ContinuousLinearMap.toSpanSingletonLIE ℝ EulerSmoothLimit.Space).toLinearIsometry.toContinuousLinearMap

theorem EulerSourcePotentialCoefficient.columnPath_norm {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : ‖columnPath‖ ≤ 1

theorem EulerSourcePotentialCoefficient.columnPath_translation {K : Type u_1} [TopologicalSpace K] (A : C(K, BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)) (a : EulerSmoothLimit.Space) : EulerMeanCoefficients.translateCoefficientPath (columnPath A) a = columnPath (EulerMeanCoefficients.translateCoefficientPath A a)

noncomputable def EulerSourcePotentialCoefficient.potentialTimePath {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (m : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (m₁ : C(K, BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (y : EulerSmoothLimit.Space), c ≤ ‖(m.field t) y‖ ^ 2) : C(K, PotentialField)

Potential time path, given by potentialPathMap (timeNormalPath (normalFunctional m c hc hm) (columnPath m₁)).

Equations

• One or more equations did not get rendered due to their size.

theorem EulerSourcePotentialCoefficient.potentialTimePath_apply {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (m : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (m₁ : C(K, BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (y : EulerSmoothLimit.Space), c ≤ ‖(m.field t) y‖ ^ 2) (t : K) (y : EulerSmoothLimit.Space) : ((potentialTimePath m m₁ c hc hm) t) y = EulerPacketCrossProduct.potentialMultiplierDerivative ((m.field t) y) ((m₁ t) y)

theorem EulerSourcePotentialCoefficient.potentialTimePath_translation {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (m : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (m₁ : C(K, BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (y : EulerSmoothLimit.Space), c ≤ ‖(m.field t) y‖ ^ 2) : EulerMeanCoefficients.translateCoefficientPath (potentialTimePath m m₁ c hc hm) = fun (a : EulerSmoothLimit.Space) => potentialPathMap (timeNormalPath (EulerMeanCoefficients.translateCoefficientPath (EulerSourceNormalCoefficient.normalFunctional m c hc hm) a) (columnPath (EulerMeanCoefficients.translateCoefficientPath m₁ a)))

theorem EulerSourcePotentialCoefficient.potentialTimePath_orbit {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (m : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (m₁ : C(K, BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (y : EulerSmoothLimit.Space), c ≤ ‖(m.field t) y‖ ^ 2) (h₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath m₁)) : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath (potentialTimePath m m₁ c hc hm))

theorem EulerSourcePotentialCoefficient.potentialTimePath_bound {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (m : EulerMeanCoefficients.SmoothCoefficientPath K EulerSmoothLimit.Space) (m₁ : C(K, BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : K) (y : EulerSmoothLimit.Space), c ≤ ‖(m.field t) y‖ ^ 2) (h₁ : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath m₁)) (R C D : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hD : 0 ≤ D) (hbN : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (EulerSourceNormalCoefficient.normalFunctional m c hc hm)) a‖ ≤ C * EulerGevrey.majorant R 0 n) (hb₁ : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath m₁) a‖ ≤ D * EulerGevrey.majorant R 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath (potentialTimePath m m₁ c hc hm)) a‖ ≤ 27 * C ^ 2 * D * EulerGevrey.majorant R 0 n

theorem EulerSourcePotentialCoefficient.potentialTimePath_hasDerivWithinAt (T : ℝ) (hT : 0 ≤ T) (m : EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 T)) EulerSmoothLimit.Space) (m₁ : C(↑(Set.Icc 0 T), BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)) (c : ℝ) (hc : 0 < c) (hm : ∀ (t : ↑(Set.Icc 0 T)) (y : EulerSmoothLimit.Space), c ≤ ‖(m.field t) y‖ ^ 2) (hmt : ∀ t ∈ Set.Icc 0 T, ∀ (y : EulerSmoothLimit.Space), HasDerivWithinAt (fun (r : ℝ) => (EulerVolterraConvolution.extendPath T hT m.field r) y) ((EulerVolterraConvolution.extendPath T hT m₁ t) y) (Set.Icc 0 T) t) (t : ↑(Set.Icc 0 T)) (y : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (r : ℝ) => (EulerVolterraConvolution.extendPath T hT (potentialCoefficient m c hc hm) r) y) (((potentialTimePath m m₁ c hc hm) t) y) (Set.Icc 0 T) ↑t

Genuine time derivatives of the inverse deformation and its transported normal.

@[instance_reducible]

noncomputable def EulerDeformationTime.instDeformationTimeInverse1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerDeformationTime.instDeformationTimeInverse1 = inferInstance

@[instance_reducible]

noncomputable def EulerDeformationTime.instDeformationTimeInverse2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerDeformationTime.instDeformationTimeInverse2 = inferInstance

def EulerDeformationTime.inverseUnit (F G : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hFG : F ∘SL G = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space) (hGF : G ∘SL F = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space) : (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)ˣ

Inverse unit, bundling val, inv, val_inv, inv_val.

Equations

• EulerDeformationTime.inverseUnit F G hFG hGF = { val := F, inv := G, val_inv := hFG, inv_val := hGF }

theorem EulerDeformationTime.inverse_hasDerivWithinAt (s : Set ℝ) (t : ℝ) (ht : t ∈ s) (F G : ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (F₁ : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hFG : ∀ r ∈ s, F r ∘SL G r = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space) (hGF : ∀ r ∈ s, G r ∘SL F r = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space) (hF : HasDerivWithinAt F F₁ s t) : HasDerivWithinAt G (-G t ∘SL F₁ ∘SL G t) s t

theorem EulerDeformationTime.inverse_strain_hasDerivWithinAt (s : Set ℝ) (t : ℝ) (ht : t ∈ s) (F G : ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hFG : ∀ r ∈ s, F r ∘SL G r = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space) (hGF : ∀ r ∈ s, G r ∘SL F r = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space) (hF : HasDerivWithinAt F (M ∘SL F t) s t) : HasDerivWithinAt G (-G t ∘SL M) s t

F_t=MF implies (F⁻¹)_t=−F⁻¹M on the same closed time set.

noncomputable def EulerDeformationTime.adjointVector (m₀ : EulerSmoothLimit.Space) : (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) →L[ℝ] EulerSmoothLimit.Space

Adjoint vector as an element of (Space →L[ℝ] Space) →L[ℝ] Space.

Equations

• EulerDeformationTime.adjointVector m₀ = (ContinuousLinearMap.apply ℝ EulerSmoothLimit.Space) m₀ ∘SL ↑↑ContinuousLinearMap.adjoint

theorem EulerDeformationTime.normal_hasDerivWithinAt (s : Set ℝ) (t : ℝ) (ht : t ∈ s) (F G : ℝ → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (M : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (m₀ : EulerSmoothLimit.Space) (hFG : ∀ r ∈ s, F r ∘SL G r = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space) (hGF : ∀ r ∈ s, G r ∘SL F r = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space) (hF : HasDerivWithinAt F (M ∘SL F t) s t) : HasDerivWithinAt (fun (r : ℝ) => (ContinuousLinearMap.adjoint (G r)) m₀) (-(ContinuousLinearMap.adjoint M) ((ContinuousLinearMap.adjoint (G t)) m₀)) s t

The actual transported normal satisfies m_t=−M* m.

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketTimeData1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerTransversePacketProvider.Data.instTransversePacketTimeData1 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketTimeData2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerTransversePacketProvider.Data.instTransversePacketTimeData2 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketTimeData3 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerTransversePacketProvider.Data.instTransversePacketTimeData3 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketTimeData4 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerTransversePacketProvider.Data.instTransversePacketTimeData4 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketTimeData5 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : NormedAddCommGroup C(↑(Set.Icc 0 D.T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) D.T,Space →ᵇ Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• D.instTransversePacketTimeData5 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketTimeData6 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : NormedSpace ℝ C(↑(Set.Icc 0 D.T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) D.T,Space →ᵇ Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• D.instTransversePacketTimeData6 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketTimeData7 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)

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

Equations

• EulerTransversePacketProvider.Data.instTransversePacketTimeData7 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketTimeData8 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)

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

Equations

• EulerTransversePacketProvider.Data.instTransversePacketTimeData8 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketTimeData9 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : NormedAddCommGroup C(↑(Set.Icc 0 D.T), BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) D.T,Space →ᵇ Space) instance to shorten typeclass synthesis.

Equations

• D.instTransversePacketTimeData9 = inferInstance

@[instance_reducible]

noncomputable def EulerTransversePacketProvider.Data.instTransversePacketTimeData10 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : NormedSpace ℝ C(↑(Set.Icc 0 D.T), BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) D.T,Space →ᵇ Space) instance to shorten typeclass synthesis.

Equations

• D.instTransversePacketTimeData10 = inferInstance

noncomputable def EulerTransversePacketProvider.Data.inverseDerivative {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : C(↑(Set.Icc 0 D.T), BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

The derivative of the inverse is constructed from the original fields.

Equations

• D.inverseDerivative = -(EulerBoundedFieldCalculus.pathCompositionMap D.FInv.field) D.M.field

noncomputable def EulerTransversePacketProvider.Data.normalDerivative {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : C(↑(Set.Icc 0 D.T), BoundedContinuousFunction EulerSmoothLimit.Space EulerSmoothLimit.Space)

The derivative of the transported normal is the fixed adjoint-vector map of that path.

Equations

• D.normalDerivative = (EulerMeanCoefficients.mapCoefficientPath (EulerTransverseBoundedFrame.normalMap D.m₀)) D.inverseDerivative

@[simp]

theorem EulerTransversePacketProvider.Data.inverseDerivative_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : (D.inverseDerivative t) x = -(D.FInv.field t) x ∘SL (D.M.field t) x

@[simp]

theorem EulerTransversePacketProvider.Data.normalDerivative_apply {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : (D.normalDerivative t) x = -(ContinuousLinearMap.adjoint ((D.M.field t) x)) ((D.normal.field t) x)

theorem EulerTransversePacketProvider.Data.inverse_hasDerivWithinAt {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ℝ) (ht : t ∈ Set.Icc 0 D.T) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (r : ℝ) => (EulerVolterraConvolution.extendPath D.T ⋯ D.FInv.field r) x) ((EulerVolterraConvolution.extendPath D.T ⋯ D.inverseDerivative t) x) (Set.Icc 0 D.T) t

No differentiability of F⁻¹ is assumed: it follows from the actual inverse identities and F_t=MF.

theorem EulerTransversePacketProvider.Data.normal_hasDerivWithinAt {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ℝ) (ht : t ∈ Set.Icc 0 D.T) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (r : ℝ) => (EulerVolterraConvolution.extendPath D.T ⋯ D.normal.field r) x) ((EulerVolterraConvolution.extendPath D.T ⋯ D.normalDerivative t) x) (Set.Icc 0 D.T) t

theorem EulerTransversePacketProvider.Data.inverseDerivative_translation {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : EulerMeanCoefficients.translateCoefficientPath D.inverseDerivative = fun (a : EulerSmoothLimit.Space) => -(EulerBoundedFieldCalculus.pathCompositionMap (EulerMeanCoefficients.translateCoefficientPath D.FInv.field a)) (EulerMeanCoefficients.translateCoefficientPath D.M.field a)

theorem EulerTransversePacketProvider.Data.normalDerivative_translation {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : EulerMeanCoefficients.translateCoefficientPath D.normalDerivative = fun (a : EulerSmoothLimit.Space) => (EulerMeanCoefficients.mapCoefficientPath (EulerTransverseBoundedFrame.normalMap D.m₀)) (EulerMeanCoefficients.translateCoefficientPath D.inverseDerivative a)

theorem EulerTransversePacketProvider.Data.inverseDerivative_orbit {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.inverseDerivative)

theorem EulerTransversePacketProvider.Data.normalDerivative_orbit {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.normalDerivative)

theorem EulerTransversePacketProvider.Data.normalPathMap_norm {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : ‖EulerMeanCoefficients.mapCoefficientPath (EulerTransverseBoundedFrame.normalMap D.m₀)‖ ≤ 1

theorem EulerTransversePacketProvider.Data.inverseDerivative_bound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (R CI CM : ℝ) (hR : 0 ≤ R) (hCI : 0 ≤ CI) (hCM : 0 ≤ CM) (hI : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.FInv.field) a‖ ≤ CI * EulerGevrey.majorant R 0 n) (hM : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.M.field) a‖ ≤ CM * EulerGevrey.majorant R 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.inverseDerivative) a‖ ≤ 3 * CI * CM * EulerGevrey.majorant R 0 n

theorem EulerTransversePacketProvider.Data.normalDerivative_bound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (R CI CM : ℝ) (hR : 0 ≤ R) (hCI : 0 ≤ CI) (hCM : 0 ≤ CM) (hI : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.FInv.field) a‖ ≤ CI * EulerGevrey.majorant R 0 n) (hM : ∀ (n : ℕ) (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.M.field) a‖ ≤ CM * EulerGevrey.majorant R 0 n) (n : ℕ) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath D.normalDerivative) a‖ ≤ 3 * CI * CM * EulerGevrey.majorant R 0 n

noncomputable def EulerTransversePacketProvider.Data.potentialDerivative {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : C(↑(Set.Icc 0 D.T), EulerSourcePotentialCoefficient.PotentialField)

The actual time coefficient for the periodic-potential multiplier.

Equations

• D.potentialDerivative = EulerSourcePotentialCoefficient.potentialTimePath D.normal D.normalDerivative D.normalLower ⋯ ⋯

theorem EulerTransversePacketProvider.Data.potentialDerivative_orbit {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath D.potentialDerivative)

theorem EulerTransversePacketProvider.Data.potential_hasDerivWithinAt {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : Data U) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : HasDerivWithinAt (fun (r : ℝ) => (EulerVolterraConvolution.extendPath D.T ⋯ (EulerSourcePotentialCoefficient.potentialCoefficient D.normal D.normalLower ⋯ ⋯) r) x) ((D.potentialDerivative t) x) (Set.Icc 0 D.T) ↑t