The constructed source coordinate propagator is an actual physical tangent solution after multiplication by F R. Consequently a physical propagator estimate supplies H3 with only the explicit F and F⁻¹ factors, preserving exactly the time-profile ratio.

@[instance_reducible]

def EulerPacketSourcePropagator.instPacketSourcePropagator1 {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] : NormedSpace ℝ U

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

Equations

• EulerPacketSourcePropagator.instPacketSourcePropagator1 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketSourcePropagator.instPacketSourcePropagator2 : NormedAddCommGroup EulerSmoothLimit.Space

Cache the standard NormedAddCommGroup Space instance to shorten typeclass synthesis.

Equations

• EulerPacketSourcePropagator.instPacketSourcePropagator2 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketSourcePropagator.instPacketSourcePropagator3 : NormedSpace ℝ EulerSmoothLimit.Space

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

Equations

• EulerPacketSourcePropagator.instPacketSourcePropagator3 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketSourcePropagator.instPacketSourcePropagator4 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketSourcePropagator.instPacketSourcePropagator5 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketSourcePropagator.instPacketSourcePropagator6 {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.instPacketSourcePropagator6 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketSourcePropagator.instPacketSourcePropagator7 = inferInstance

@[instance_reducible]

noncomputable def EulerPacketSourcePropagator.instPacketSourcePropagator8 {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.instPacketSourcePropagator8 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketSourcePropagator.instPacketSourcePropagator9 = inferInstance

@[reducible, inline]

noncomputable abbrev EulerPacketSourcePropagator.fundamental {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) : EulerLinearFundamentalExistence.FundamentalPath D.T ⋯ (EulerSourceForwardCoefficient.sourceGenerator D.frame D.frameDerivative D.frameLower ⋯ ⋯)

Fundamental: an abbreviation for fundamentalPath D.T D.T_pos.le (sourceGenerator D.frame D.frameDerivative D.frameLower D.frameLower_pos D.frame_lower).

Equations

• EulerPacketSourcePropagator.fundamental D = EulerLinearFundamentalExistence.fundamentalPath D.T ⋯ (EulerSourceForwardCoefficient.sourceGenerator D.frame D.frameDerivative D.frameLower ⋯ ⋯)

noncomputable def EulerPacketSourcePropagator.propagator {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (t s : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : U →L[ℝ] U

Propagator, given by ((fundamental D).forward t x).comp ((fundamental D).backward s x).

Equations

• EulerPacketSourcePropagator.propagator D t s x = ((EulerPacketSourcePropagator.fundamental D).forward t) x ∘SL ((EulerPacketSourcePropagator.fundamental D).backward s) x

noncomputable def EulerPacketSourcePropagator.coordinate {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (s : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (v : U) (t : ℝ) : U

Coordinate, given by extendPath D.T D.T_pos.le (fundamental D).forward t x ((fundamental D).backward s x v).

Equations

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

noncomputable def EulerPacketSourcePropagator.physical {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (s : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (v : U) (t : ℝ) : EulerSmoothLimit.Space

Physical, given by extendPath D.T D.T_pos.le D.frame.field t x (coordinate D s x v t).

Equations

• EulerPacketSourcePropagator.physical D s x v t = ((EulerVolterraConvolution.extendPath D.T ⋯ D.frame.field t) x) (EulerPacketSourcePropagator.coordinate D s x v t)

noncomputable def EulerPacketSourcePropagator.physicalRhs {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (t : ↑(Set.Icc 0 D.T)) (x w : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Physical rhs, given by -(D.M.field t x) w + (2*⟪D.normal.field t x,(D.M.field t x) w⟫_ℝ/‖D.normal.field t x‖^2) • D.normal.field t x.

Equations

• EulerPacketSourcePropagator.physicalRhs D t x w = -((D.M.field t) x) w + (2 * inner ℝ ((D.normal.field t) x) (((D.M.field t) x) w) / ‖(D.normal.field t) x‖ ^ 2) • (D.normal.field t) x

@[simp]

theorem EulerPacketSourcePropagator.coordinate_at {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (s t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (v : U) : coordinate D s x v ↑t = (propagator D t s x) v

@[simp]

theorem EulerPacketSourcePropagator.physical_at {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (s t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (v : U) : physical D s x v ↑t = ((D.frame.field t) x) ((propagator D t s x) v)

@[simp]

theorem EulerPacketSourcePropagator.propagator_self {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (s : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (v : U) : (propagator D s s x) v = v

theorem EulerPacketSourcePropagator.physical_tangent {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (s t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (v : U) : inner ℝ ((D.normal.field t) x) (physical D s x v ↑t) = 0

theorem EulerPacketSourcePropagator.coordinate_hasDerivWithinAt {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (s t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (v : U) : HasDerivWithinAt (coordinate D s x v) ((((EulerSourceForwardCoefficient.sourceGenerator D.frame D.frameDerivative D.frameLower ⋯ ⋯) t) x) (coordinate D s x v ↑t)) (Set.Icc 0 D.T) ↑t

theorem EulerPacketSourcePropagator.physical_hasDerivWithinAt {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (s t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (v : U) : HasDerivWithinAt (physical D s x v) (physicalRhs D t x (physical D s x v ↑t)) (Set.Icc 0 D.T) ↑t

def EulerPacketSourcePropagator.PhysicalGrowth {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] (D : EulerTransversePacketProvider.Data U) (S : Set EulerSmoothLimit.Space) (g : ↑(Set.Icc 0 D.T) → ℝ) (C : ℝ) : Prop

A physical growth assertion is tested only on genuine solutions of the literal tangent ODE, with the actual transported normal.

Equations

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

theorem EulerPacketSourcePropagator.propagator_bound_of_physical {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (S : Set EulerSmoothLimit.Space) (g : ↑(Set.Icc 0 D.T) → ℝ) (hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t) (C F I : ℝ) (hC : 0 ≤ C) (hF : 0 ≤ F) (hI : 0 ≤ I) (hphysical : PhysicalGrowth D S g C) (hframe : ∀ (t : ↑(Set.Icc 0 D.T)), ∀ x ∈ S, ‖(D.F.field t) x‖ ≤ F) (hinverse : ∀ (t : ↑(Set.Icc 0 D.T)), ∀ x ∈ S, ‖(D.FInv.field t) x‖ ≤ I) (t s : ↑(Set.Icc 0 D.T)) (hst : s ≤ t) (x : EulerSmoothLimit.Space) (hx : x ∈ S) : ‖propagator D t s x‖ ≤ I * C * F * g t / g s

Coordinate norms cost precisely the inverse deformation at the final time and deformation at the initial time. No extremum of g is used.

theorem EulerPacketSourcePropagator.propagator_bound_of_deformation {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (S : Set EulerSmoothLimit.Space) (g : ↑(Set.Icc 0 D.T) → ℝ) (hg : ∀ (t : ↑(Set.Icc 0 D.T)), 0 < g t) (C F : ℝ) (hC : 0 ≤ C) (hF : 0 ≤ F) (hphysical : PhysicalGrowth D S g C) (hdet : ∀ (t : ↑(Set.Icc 0 D.T)), ∀ x ∈ S, Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1) (hframe : ∀ (t : ↑(Set.Icc 0 D.T)), ∀ x ∈ S, ‖(D.F.field t) x‖ ≤ F) (t s : ↑(Set.Icc 0 D.T)) (hst : s ≤ t) (x : EulerSmoothLimit.Space) (hx : x ∈ S) : ‖propagator D t s x‖ ≤ 3 * F ^ 3 * C * g t / g s

For det F=1, the inverse factor is a proved cofactor bound. Thus the physical propagator constant C becomes the polynomial 3 F³ C in H3.