Actual parent fields and the physical tangent growth estimate supply the complete joined-packet input at one common radius. The history Jacobi law, inverse coefficients and all coefficient matches are proved.
structure
EulerParentPacketFrames.JoinedInputs
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(M : EulerMeanPacketProvider.Data)
(D : EulerTransversePacketProvider.Data U)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
:
Joined inputs data, collecting linear, normal, mean.
- linear : EulerTransversePacketJoin.Budget D τ hτ hτT H (Fin 4) 6
Linear of
JoinedInputs, of typeEulerTransversePacketJoin.Budget D τ hτ hτT H (Fin 4) 6. - normal : EulerTransversePacketJoin.NormalBudget D 6 self.linear.R
Normal of
JoinedInputs, of typeEulerTransversePacketJoin.NormalBudget D 6 linear.R. - mean : EulerMeanPacketProvider.Budget M 6 self.linear.R
Mean field of
JoinedInputs, of typeEulerMeanPacketProvider.Budget M 6 linear.R.
Instances For
noncomputable def
EulerParentPacketFrames.Parent.historyOn
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(G : Parent)
(H : LowBounds G)
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < G.T)
:
EulerTransversePacketProvider.HistoryData ((G.transverseData m hm R S hS).initial τ hτ ⋯)
History on, given by (G.historyData m hm R S hS H).initial τ hτ hτT.le.
Equations
- G.historyOn H m hm R S hS τ hτ hτT = (G.historyData m hm R S hS H).initial τ hτ ⋯
Instances For
noncomputable def
EulerParentPacketFrames.Parent.secondInitial
(G : Parent)
(τ : ℝ)
(hτT : τ < G.T)
:
Second initial, given by G.second.toSmoothCoefficientPath.comp (initialInclusion G.T τ hτT.le).
Equations
- G.secondInitial τ hτT = G.second.toSmoothCoefficientPath.comp (EulerTimeIntervalRestriction.initialInclusion G.T τ ⋯)
Instances For
theorem
EulerParentPacketFrames.Parent.secondInitial_derivative
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(G : Parent)
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < G.T)
(t : ℝ)
(ht : t ∈ Set.Icc 0 τ)
(x : EulerSmoothLimit.Space)
:
HasDerivWithinAt
(fun (s : ℝ) =>
(EulerVolterraConvolution.extendPath τ ⋯ ((G.transverseData m hm R S hS).initial τ hτ ⋯).F₁.field s) x)
((EulerVolterraConvolution.extendPath τ ⋯ (G.secondInitial τ hτT).field t) x) (Set.Icc 0 τ) t
noncomputable def
EulerParentPacketFrames.LabelData.joinedRaw
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{G : Parent}
(L : LabelData G)
(H : LowBounds G)
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < G.T)
(Ti Cp : ℝ)
(hτ1 : τ ≤ 1)
(hTi : τ⁻¹ ≤ Ti)
(hCp : 0 ≤ Cp)
(g : C(↑(Set.Icc 0 (G.T - τ)), ℝ))
(hg : ∀ (t : ↑(Set.Icc 0 (G.T - τ))), 0 < g t)
(hg0 : g ⟨0, ⋯⟩ = 1)
(Ω : Set EulerSmoothLimit.Space)
(hΩ : MeasurableSet Ω)
(hΩo : IsOpen Ω)
(hsub : S ⊆ Ω)
(hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2)
(hphysical :
EulerPacketSourcePropagator.PhysicalGrowth ((G.transverseData m hm R S hS).tail τ ⋯ hτT)
EulerPacketParentPhysicalBudgets.halfBall (⇑g) Cp)
:
EulerTransversePacketJoin.Budget (G.transverseData m hm R S hS) τ hτ hτT (G.historyOn H m hm R S hS τ hτ hτT) (Fin 4) 6
Joined raw, constructed using EulerPacketParentPhysicalBudgets.joinedBudget.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerParentPacketFrames.LabelData.joinedInputs
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{G : Parent}
(L : LabelData G)
(H : LowBounds G)
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < G.T)
(Ti Cp : ℝ)
(hτ1 : τ ≤ 1)
(hTi : τ⁻¹ ≤ Ti)
(hCp : 0 ≤ Cp)
(g : C(↑(Set.Icc 0 (G.T - τ)), ℝ))
(hg : ∀ (t : ↑(Set.Icc 0 (G.T - τ))), 0 < g t)
(hg0 : g ⟨0, ⋯⟩ = 1)
(Ω : Set EulerSmoothLimit.Space)
(hΩ : MeasurableSet Ω)
(hΩo : IsOpen Ω)
(hsub : S ⊆ Ω)
(hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2)
(hphysical :
EulerPacketSourcePropagator.PhysicalGrowth ((G.transverseData m hm R S hS).tail τ ⋯ hτT)
EulerPacketParentPhysicalBudgets.halfBall (⇑g) Cp)
(TiTotal : ℝ)
(hT1 : G.T ≤ 1)
(hTiTotal : G.T⁻¹ ≤ TiTotal)
:
JoinedInputs (G.meanData H) (G.transverseData m hm R S hS) τ hτ hτT (G.historyOn H m hm R S hS τ hτ hτT)
Joined inputs as an element of JoinedInputs (G.meanData H) (G.transverseData m hm R S hS) τ hτ hτT (G.historyOn H m hm R S hS τ hτ hτT).
Equations
- One or more equations did not get rendered due to their size.