Both actual initialized packet branches produce the same recursive physical state. Their residual and parity proofs are supplied by their source formulas, not additional hypotheses about the new solution.
noncomputable def
EulerParentPacketFrames.SmoothState.forwardChild
{A : Parent}
(S : SmoothState A)
(H : LowBounds A)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(support : Set EulerSmoothLimit.Space)
(hSupport : IsCompact support)
(hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ support ↔ x ∈ support)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support)
(α : ℝ)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(Q :
EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯
(EulerPacketTerminalDatum.forwardInitializedCorrectionData (A.meanData H) (A.transverseData m hm J support hSupport)
⋯ δ hδ ξ hs α ⋯ N hN k hk))
(G : EulerPhysicalGraphFlowBounds.Data EulerPacketTerminalDatum.period A.T)
(hG :
G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient EulerPacketTerminalDatum.period Q
(EulerPacketTerminalDatum.forwardInitializedNormalizedField (A.meanData H)
(A.transverseData m hm J support hSupport) ⋯ δ hδ ξ hs α N k))
(hgraph :
∀ (t : ↑(Set.Icc 0 A.T)) (q : EulerLiftedGradientSpace.LiftTangent),
(EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) q) = 0)
(nextEll : ℝ)
(hnext : 0 < nextEll)
(hnext1 : nextEll ≤ 1)
(labels : LabelData (A.child G k m hgraph nextEll hnext hnext1))
:
SmoothState (A.child G k m hgraph nextEll hnext hnext1)
Forward child, constructed using S.packetChild.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerParentPacketFrames.SmoothState.joinedChild
{A : Parent}
(S : SmoothState A)
(H : LowBounds A)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(J : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(support : Set EulerSmoothLimit.Space)
(hSupport : IsCompact support)
(hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ support ↔ x ∈ support)
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ support)
(α : ℝ)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < A.T)
(Q :
EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯
(EulerPacketTerminalDatum.initializedCorrectionData (A.meanData H) (A.transverseData m hm J support hSupport) ⋯ τ hτ
hτT (A.historyOn H m hm J support hSupport τ hτ hτT) δ hδ ξ hs α ⋯ N hN k hk))
(G : EulerPhysicalGraphFlowBounds.Data EulerPacketTerminalDatum.period A.T)
(hG :
G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient EulerPacketTerminalDatum.period Q
(EulerPacketTerminalDatum.initializedNormalizedField (A.meanData H) (A.transverseData m hm J support hSupport) ⋯ τ
hτ hτT (A.historyOn H m hm J support hSupport τ hτ hτT) δ hδ ξ hs α N k))
(hgraph :
∀ (t : ↑(Set.Icc 0 A.T)) (q : EulerLiftedGradientSpace.LiftTangent),
(EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) q) = 0)
(nextEll : ℝ)
(hnext : 0 < nextEll)
(hnext1 : nextEll ≤ 1)
(labels : LabelData (A.child G k m hgraph nextEll hnext hnext1))
:
SmoothState (A.child G k m hgraph nextEll hnext hnext1)
Joined child, constructed using S.packetChild.
Equations
- One or more equations did not get rendered due to their size.