The scalar induction guards apply to the actual parent source data. History norms and symmetry are derived from the parent fields, and the neighbor error is the computed, ell-scaled coefficient expression.
theorem
EulerPacketSourceGeometry.ParentFrame.activation_normal_le
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{τ : ℝ}
(P : ParentFrame D τ)
(hτ : 0 < τ)
(hτT : τ < D.T)
:
inner ℝ (((D.M.field ⟨τ, ⋯⟩) 0) (EulerPacketNormalizedPrimary.unit (P.m τ)))
(EulerPacketNormalizedPrimary.unit (P.m τ)) ≤ inner ℝ ((P.B τ) (EulerPacketNormalizedPrimary.unit (P.m τ))) (EulerPacketNormalizedPrimary.unit (P.m τ)) + P.error
theorem
EulerPacketSourceGeometry.ParentFrame.activation_compression_of_previous
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{τ : ℝ}
(P : ParentFrame D τ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(e : ℝ)
(he : P.error ≤ e)
(hprevious :
inner ℝ ((P.B τ) (EulerPacketNormalizedPrimary.unit (P.m τ))) (EulerPacketNormalizedPrimary.unit (P.m τ)) + e < 0)
:
noncomputable def
EulerParentPacketFrames.LabelData.historyAmplitude
{G : Parent}
(L : LabelData G)
:
One explicit parent coefficient amplitude controls both the actual strain and pressure Hessian throughout the history interval.
Equations
Instances For
theorem
EulerParentPacketFrames.LabelData.history_strain_norm
{G : Parent}
(L : LabelData G)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(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 : ↑(Set.Icc 0 τ))
(x : EulerSmoothLimit.Space)
:
theorem
EulerParentPacketFrames.LabelData.history_hessian_norm
{G : Parent}
(L : LabelData G)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(H : LowBounds G)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < G.T)
(x : EulerSmoothLimit.Space)
:
noncomputable def
EulerParentPacketFrames.LabelData.geometryGuardsOfStage
{G : Parent}
(L : LabelData G)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(H : LowBounds G)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < G.T)
(P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) τ)
(p : ↑(Set.Icc 0 G.T) → EulerSmoothLimit.Space → ℝ)
(hp : ∀ (t : ↑(Set.Icc 0 G.T)), ContDiff ℝ (↑⊤) (p t))
(hacc :
∀ (t : ↑(Set.Icc 0 G.T)) (x : EulerSmoothLimit.Space), (G.acceleration.field t) x = -gradient (p t) (G.position t x))
(J D : ℕ)
(C c X : ℝ)
(a β : ℕ → ℝ)
(n : ℕ)
(hX : 0 < X)
(CF : ℝ)
(hCF : 1 ≤ CF)
(stage :
EulerPacketSourceScaleGuards.StageGuards J D C c X (EulerPacketMovingFrame.neighborStabilityConstant * CF ^ 2) a β n)
(ha : 1 / 2 ≤ a n)
(ha_match : P.a = a n)
(hshear : P.shear = EulerPacketSourceScaleSequence.previousShear J X n)
(hsigma : P.sigma = √(β n))
(htime : P.horizon = EulerPacketSourceScaleGuards.horizon J X (a n) (β n) n)
(hG : P.G ≤ CF * (1 + EulerPacketSourceScaleSequence.olderShear J X n))
(herr : P.error ≤ EulerPacketSourceScaleActual.priorError J D X n)
(CM CH ζ ρ δ hchild : ℝ)
(hCM : 0 ≤ CM)
(hCH : 0 ≤ CH)
(hζ : 0 ≤ ζ)
(hρ : 0 ≤ ρ)
(hδ : 0 ≤ δ)
(hhchild : 0 ≤ hchild)
(hneighbor :
L.neighborScaleCost m hm R S hS H τ hτ hτT P CM CH * G.ell * ρ ≤ EulerPacketSourceScaleActual.neighborError J D X c n)
(hnormal :
m = EulerPacketMovingFrame.activationDirection ((G.transverseData m hm R S hS).deformationEquiv ⟨τ, ⋯⟩ 0)
(EulerPacketCrossProduct.cross (EulerPacketNormalizedPrimary.unit (P.m τ))
(EulerPacketNormalizedPrimary.unit (P.v τ))))
(hlayer : 1 ≤ EulerPacketSourceScaleSequence.previousShear J X n * τ)
(hstrain :
‖(EulerTransverseSourceCoefficientPath.pathEvaluation 0) ((G.transverseData m hm R S hS).initial τ hτ ⋯).M.field‖ ≤ CM * EulerPacketSourceScaleSequence.previousShear J X n)
(hhessian :
‖(G.historyOn H m hm R S hS τ hτ hτT).coefficients.labelHessian 0‖ ≤ CH * EulerPacketSourceScaleSequence.previousShear J X n ^ 2)
(hactivation : 16 * (EulerTransverseActivationSelection.activationConstant CM CH + 1) * ζ ≤ 1)
(hactivationError :
CF * (1 + EulerPacketSourceScaleSequence.olderShear J X n) + EulerPacketSourceScaleActual.priorError J D X n ≤ ζ * EulerPacketSourceScaleSequence.previousShear J X n)
(hpreviousCompression :
inner ℝ ((P.B τ) (EulerPacketNormalizedPrimary.unit (P.m τ))) (EulerPacketNormalizedPrimary.unit (P.m τ)) + EulerPacketSourceScaleActual.priorError J D X n < 0)
:
EulerPacketSourceGeometry.Guards hτ hτT P (G.historyOn H m hm R S hS τ hτ hτT)
Apply the manuscript's scalar stage bounds to the literal source coefficients. The remaining inputs are older-stage center data, the chosen normal, and scalar comparisons with explicit source costs.
Equations
- One or more equations did not get rendered due to their size.