The source tangent equation is a reflection of the strain applied to the velocity. Its actual norm is therefore unchanged by the normal factor. A short interval controlled by the low strain norm supplies H3 with g=1.

theorem EulerPacketSourcePropagator.normal_reflection_norm {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (m r : E) : ‖-r + (2 * inner ℝ m r / ‖m‖ ^ 2) • m‖ = ‖r‖

theorem EulerPacketSourcePropagator.physicalRhs_norm {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (t : ↑(Set.Icc 0 D.T)) (x w : EulerSmoothLimit.Space) : ‖physicalRhs D t x w‖ = ‖((D.M.field t) x) w‖

theorem EulerPacketSourcePropagator.physicalGrowth_one_of_short {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (S : Set EulerSmoothLimit.Space) (C : ℝ) (hC : 0 ≤ C) (hM : ∀ (t : ↑(Set.Icc 0 D.T)), ∀ x ∈ S, ‖(D.M.field t) x‖ ≤ C) (hshort : C * D.T ≤ 1 / 2) : PhysicalGrowth D S (fun (x : ↑(Set.Icc 0 D.T)) => 1) 2

No inverse normal bound or all-order coefficient norm occurs in the shortness condition. The derivative equation is required literally.

@[instance_reducible]

noncomputable def EulerPacketSourcePropagator.instPacketShortTimePhysicalGrowth1 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedRing (U →L[ℝ] U)

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

Equations

• EulerPacketSourcePropagator.instPacketShortTimePhysicalGrowth1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketSourcePropagator.instPacketShortTimePhysicalGrowth2 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedRing (BoundedContinuousFunction EulerSmoothLimit.Space (U →L[ℝ] U))

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

Equations

• EulerPacketSourcePropagator.instPacketShortTimePhysicalGrowth2 = inferInstance

def EulerPacketSourcePropagator.shortPhysicalForwardBudget {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (q : ℕ) (R C C₁ CM : ℝ) (hR : 0 ≤ R) (hC : 0 ≤ C) (hC₁ : 0 ≤ C₁) (hCM : 0 ≤ CM) (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) (hF₁ : ∀ (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (⇑(D.F₁.field t)) x‖ ≤ C₁ * EulerGevrey.majorant R 0 n) (hM : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), ‖x‖ ≤ 1 / 2 → ‖(D.M.field t) x‖ ≤ CM) (Ω : Set EulerSmoothLimit.Space) (hΩ : MeasurableSet Ω) (hΩo : IsOpen Ω) (hsub : D.support ⊆ Ω) (hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2) (hshort : CM * D.T ≤ 1 / 2) : EulerTransversePacketForward.Budget D (Fin 4) q

A low strain bound on the H3 ball suffices for the entire source forward budget. The coordinate propagation cost is the polynomial 6 C³.

Equations

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