Actual activation geometry and one uniform frequency comparison construct the joined packet, its physical state, and both source errors.
The uniform source comparison gives the actual child label estimate at exponent 10(q+2), retaining the same exact correction and its errors.
The actual derivative of the initialized normalized approximation has a source-dependent Gevrey bound uniform in the truncation frequency. The time derivative of the inverse deformation is included explicitly.
noncomputable def
EulerPacketTerminalDatum.initializedNormalizedDerivativeField
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(k : ℝ)
:
EulerPacketCylinderField.Field period D.T
(EulerPacketCoordinates.coordinateTime D k (initializedVelocity M D τ hτ hτT B δ hδ ξ hs α N k⁻¹)
(initializedVelocityDerivative M D τ hτ hτT B δ hδ ξ hs α N k⁻¹))
Initialized normalized derivative field, constructed using coordinateTimeField.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.initializedNormalizedField_time
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(k : ℝ)
:
EulerPacketCylinderField.TimeDerivative ⋯ (initializedNormalizedField M D hTime τ hτ hτT B δ hδ ξ hs α N k)
(initializedNormalizedDerivativeField M D hTime τ hτ hτT B δ hδ ξ hs α N k)
theorem
EulerPacketTerminalDatum.initializedNormalizedDerivativeField_bound
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(H : EulerTransversePacketPrimary.Budget L)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
(W : L.GradeGuards NB)
(LM : EulerMeanPacketProvider.Budget M 6 L.R)
(WM : LM.GradeGuards)
(BC :
EulerPacketCylinderField.CoefficientBudget
(EulerPacketCylinderField.joinedSourceCoefficientData period M D τ hτ hτT B hTime))
(hRc : EulerParameterWordGevrey.sobolevCoefficientRadius (Fin 4) BC.Rc ≤ L.R)
(hcost : BC.termCost ≤ L.R)
(hδ1 : δ ≤ 1)
(hα : 0 < α)
(hR : wordRadius (Fin 4) δ ≤ L.R)
(WP : H.GradeGuards NB (wordCost (Fin 4) 6 δ * ‖ξ‖))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.fullProfile)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase L.R S.H0 BC.termCost N ≤ k ^ (1 / 100))
:
(initializedNormalizedDerivativeField M D hTime τ hτ hτT B δ hδ ξ hs α N k).WordBound 6 (4 * L.R)
(6 * NB.blockAmplitude * (EulerPacketCylinderField.fixedVelocityGradeCost L.R S.H0 1 + EulerPacketCylinderField.fixedVelocityGradeCost L.R S.H0 2 + 1))
0
A single polynomial comparison gives the actual canonical correction, the physical shear and pressure errors, and the three flow fields. Only the displayed numerical frequency margins are independent extra guards.
theorem
EulerPacketTerminalDatum.initialized_uniform_flow_and_shear
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(hδ1 : δ ≤ 1)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(hα : 0 < α)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
{Rm : ℝ}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(W : ℝ)
(hW :
EulerPacketRadiusPolynomial.RadiusPrimitives LM L NB
(EulerPacketCylinderField.joinedCoefficientBudget period M D hTime τ hτ hτT B NB) δ ξ W)
(hprofile : ∀ (t : ↑(Set.Icc 0 D.T)), α * L.fullProfile t ≤ W)
(k : ℝ)
(hk : 4 ≤ k)
(hX : 64 ≤ EulerPacketSourceFrequency.expansion k)
(hlog : 1 ≤ Real.log k)
(hfrequency :
EulerPacketInitializedOutputCost.uniformConstant * W ^ EulerPacketInitializedOutputCost.uniformPower ≤ EulerPacketSourceFrequency.smallPower k)
(hdelta : EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ≤ k ^ (-3))
(hroot : 16 ≤ k ^ (1 / 4))
(htrace : max 71 √(2 / period + 2 * period) ≤ k ^ (1 / 24))
(X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hXs : ∀ (t : ↑(Set.Icc 0 D.T)), ContDiff ℝ (↑⊤) (X t))
(hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), fderiv ℝ (X t) x = (D.F.field t) x)
(hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x)
(hY : Continuous (Function.uncurry Y))
(hdet :
∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1)
:
∃ (hn : 1 ≤ EulerPacketSourceFrequency.truncation k) (Q :
EulerAllOrderDriftCorrection.Budget period ⋯
(initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree (EulerPacketSourceFrequency.truncation k) hn k
hk))
(G : EulerPhysicalGraphFlowBounds.Data period D.T),
Q.delta = EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ∧ Q.initialRadius = EulerPacketCorrectionScalar.initialRadius
(initializedRadius LM L NB (EulerPacketCylinderField.joinedCoefficientBudget period M D hTime τ hτ hτT B NB) δ
ξ)
(L.correctionCoefficients NB period).M (L.correctionCoefficients NB period).Rc ∧ G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient period Q
(initializedNormalizedField M D hTime τ hτ hτT B δ hδ ξ hs α (EulerPacketSourceFrequency.truncation k) k) ∧ G.A₁ = EulerAllOrderDriftCorrection.Budget.liftedPacketDerivativeCoefficient period Q
(initializedNormalizedDerivativeField M D hTime τ hτ hτT B δ hδ ξ hs α
(EulerPacketSourceFrequency.truncation k) k) ∧ (∀ (t : ↑(Set.Icc 0 D.T)) (z : EulerLiftedGradientSpace.LiftTangent),
(EulerGraphInvariantFlow.graphConstraint k D.m₀) ((G.A.field t) z) = 0) ∧ (∀ (s n : ℕ),
n + 6 ≤ s →
∀ (t : ↑(Set.Icc 0 D.T)),
EulerSobolevGevreyOperators.weightedNorm period 6 n (Q.initialRadius / 4)
(((EulerAllOrderDriftCorrection.Budget.fieldTower period Q).realization s) t) ≤ EulerPacketInitializedCost.weightSize W * EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ∧ EulerSobolevGevreyOperators.weightedNorm period 6 n (Q.initialRadius / 4)
(((EulerAllOrderDriftCorrection.Budget.pressureTower period Q).realization s) t) ≤ EulerPacketInitializedCost.weightSize W * EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ∧ EulerSobolevGevreyOperators.weightedNorm period 6 n (Q.initialRadius / 4)
(((EulerAllOrderDriftCorrection.Budget.timeDerivativeTower period Q).realization s) t) ≤ EulerPacketInitializedCost.weightSize W * EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k)) ∧ (∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
‖fderiv ℝ
(initializedExactPhysicalVelocity M D hTime τ hτ hτT B δ hδ ξ hs α Cagree
(EulerPacketSourceFrequency.truncation k) hn k hk Q t (Y t))
x - (α * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y t x))) • ((InnerProductSpace.rankOne ℝ)
(EulerPacketPrimaryFactorization.canonicalVelocity τ hτ hτT B ξ hs (↑t) (Y t x)))
((D.normal.field t) (Y t x))‖ ≤ k ^ (-(1 / 4)) ∧ ‖fderiv ℝ
(gradient
(initializedExactPhysicalPressure M D hTime τ hτ hτT B δ hδ ξ hs α Cagree
(EulerPacketSourceFrequency.truncation k) hn k hk Q t (Y t)))
x - (EulerPacketPrimaryPressure.coefficient τ hτ hτT B ξ hs α t (Y t x) * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y t x))) • ((InnerProductSpace.rankOne ℝ) ((D.normal.field t) (Y t x))) ((D.normal.field t) (Y t x))‖ ≤ k ^ (-(1 / 4))) ∧ ∀ (ell : ℝ) (hell : 0 < ell),
ell ≤ 1 →
∀ (t : ↑(Set.Icc 0 D.T)),
(G.displacementField k D.m₀ ell hell t).HasJetBound (k ^ (-(1 / 4))) (ell⁻¹ * k ^ (5 / 4)) ∧ (G.velocityField k D.m₀ ell hell t).HasJetBound (k ^ (-(1 / 4))) (ell⁻¹ * k ^ (5 / 4)) ∧ (G.accelerationFieldL2 k D.m₀ ell hell t).HasJetBound (k ^ (1 / 4)) (ell⁻¹ * k ^ (5 / 4)) ∧ EulerGevrey.HasSupBound (G.displacementField k D.m₀ ell hell t).field (k ^ (-(1 / 4)))
(ell⁻¹ * k ^ (5 / 4)) ∧ EulerGevrey.HasSupBound (G.velocityField k D.m₀ ell hell t).field (k ^ (-(1 / 4)))
(ell⁻¹ * k ^ (5 / 4))
theorem
EulerPacketTerminalDatum.initialized_uniform_child_label_bounds
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(hTime : M.T = D.T)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(hδ1 : δ ≤ 1)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(hα : 0 < α)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(NB : EulerTransversePacketJoin.NormalBudget D 6 L.R)
{Rm : ℝ}
(LM : EulerMeanPacketProvider.Budget M 6 Rm)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(W : ℝ)
(hW :
EulerPacketRadiusPolynomial.RadiusPrimitives LM L NB
(EulerPacketCylinderField.joinedCoefficientBudget period M D hTime τ hτ hτT B NB) δ ξ W)
(hprofile : ∀ (t : ↑(Set.Icc 0 D.T)), α * L.fullProfile t ≤ W)
(k : ℝ)
(hk : 4 ≤ k)
(hX : 64 ≤ EulerPacketSourceFrequency.expansion k)
(hlog : 1 ≤ Real.log k)
(hfrequency :
EulerPacketInitializedOutputCost.uniformConstant * W ^ EulerPacketInitializedOutputCost.uniformPower ≤ EulerPacketSourceFrequency.smallPower k)
(hdelta : EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ≤ k ^ (-3))
(hroot : 16 ≤ k ^ (1 / 4))
(htrace : max 71 √(2 / period + 2 * period) ≤ k ^ (1 / 24))
(X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hXs : ∀ (t : ↑(Set.Icc 0 D.T)), ContDiff ℝ (↑⊤) (X t))
(hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), fderiv ℝ (X t) x = (D.F.field t) x)
(hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x)
(hY : Continuous (Function.uncurry Y))
(hdet :
∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1)
(ell : ℝ)
(hell : 0 < ell)
(hell1 : ell ≤ 1)
(Dp Vp Wp : ↑(Set.Icc 0 D.T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space)
(K : ℝ)
(hK : 1 ≤ K)
(hDp : ∀ (t : ↑(Set.Icc 0 D.T)), EulerPacketParentLabelBounds.HasLabelBound K (Dp t))
(hVp : ∀ (t : ↑(Set.Icc 0 D.T)), EulerPacketParentLabelBounds.HasLabelBound K (Vp t))
(hWp : ∀ (t : ↑(Set.Icc 0 D.T)), EulerPacketParentLabelBounds.HasLabelBound K (Wp t))
(q : ℕ)
(hk69 : 69 ≤ k)
(hKk : K ≤ k)
(hbig : 2 + 45 * EulerPacketParentLabelBounds.embeddingCost ≤ k)
(hcost : EulerSobolevSourceExponent.fixedCost q ≤ k)
(hinv : ell⁻¹ ≤ k ^ (3 / 4))
:
∃ (hn : 1 ≤ EulerPacketSourceFrequency.truncation k) (Q :
EulerAllOrderDriftCorrection.Budget period ⋯
(initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree (EulerPacketSourceFrequency.truncation k) hn k
hk))
(G : EulerPhysicalGraphFlowBounds.Data period D.T) (E : ↑(Set.Icc 0 D.T) → EulerChildParticleFieldBounds.Data),
Q.delta = EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ∧ Q.initialRadius = EulerPacketCorrectionScalar.initialRadius
(initializedRadius LM L NB (EulerPacketCylinderField.joinedCoefficientBudget period M D hTime τ hτ hτT B NB) δ
ξ)
(L.correctionCoefficients NB period).M (L.correctionCoefficients NB period).Rc ∧ G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient period Q
(initializedNormalizedField M D hTime τ hτ hτT B δ hδ ξ hs α (EulerPacketSourceFrequency.truncation k) k) ∧ G.A₁ = EulerAllOrderDriftCorrection.Budget.liftedPacketDerivativeCoefficient period Q
(initializedNormalizedDerivativeField M D hTime τ hτ hτT B δ hδ ξ hs α
(EulerPacketSourceFrequency.truncation k) k) ∧ (∀ (t : ↑(Set.Icc 0 D.T)) (z : EulerLiftedGradientSpace.LiftTangent),
(EulerGraphInvariantFlow.graphConstraint k D.m₀) ((G.A.field t) z) = 0) ∧ (∀ (s n : ℕ),
n + 6 ≤ s →
∀ (t : ↑(Set.Icc 0 D.T)),
EulerSobolevGevreyOperators.weightedNorm period 6 n (Q.initialRadius / 4)
(((EulerAllOrderDriftCorrection.Budget.fieldTower period Q).realization s) t) ≤ EulerPacketInitializedCost.weightSize W * EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ∧ EulerSobolevGevreyOperators.weightedNorm period 6 n (Q.initialRadius / 4)
(((EulerAllOrderDriftCorrection.Budget.pressureTower period Q).realization s) t) ≤ EulerPacketInitializedCost.weightSize W * EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k) ∧ EulerSobolevGevreyOperators.weightedNorm period 6 n (Q.initialRadius / 4)
(((EulerAllOrderDriftCorrection.Budget.timeDerivativeTower period Q).realization s) t) ≤ EulerPacketInitializedCost.weightSize W * EulerPacketCorrectionScalar.delta (EulerPacketSourceFrequency.expansion k)) ∧ (∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
‖fderiv ℝ
(initializedExactPhysicalVelocity M D hTime τ hτ hτT B δ hδ ξ hs α Cagree
(EulerPacketSourceFrequency.truncation k) hn k hk Q t (Y t))
x - (α * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y t x))) • ((InnerProductSpace.rankOne ℝ)
(EulerPacketPrimaryFactorization.canonicalVelocity τ hτ hτT B ξ hs (↑t) (Y t x)))
((D.normal.field t) (Y t x))‖ ≤ k ^ (-(1 / 4)) ∧ ‖fderiv ℝ
(gradient
(initializedExactPhysicalPressure M D hTime τ hτ hτT B δ hδ ξ hs α Cagree
(EulerPacketSourceFrequency.truncation k) hn k hk Q t (Y t)))
x - (EulerPacketPrimaryPressure.coefficient τ hτ hτT B ξ hs α t (Y t x) * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y t x))) • ((InnerProductSpace.rankOne ℝ) ((D.normal.field t) (Y t x))) ((D.normal.field t) (Y t x))‖ ≤ k ^ (-(1 / 4))) ∧ (∀ (t : ↑(Set.Icc 0 D.T)),
(E t).parentDisplacement = Dp t ∧ (E t).parentVelocity = Vp t ∧ (E t).parentAcceleration = Wp t ∧ (E t).displacement = G.displacementField k D.m₀ ell hell t ∧ (E t).velocity = G.velocityField k D.m₀ ell hell t ∧ (E t).acceleration = G.accelerationFieldL2 k D.m₀ ell hell t ∧ (E t).inner = (EulerSmoothBanachFlow.flowData D.T ⋯
(EulerGraphInvariantFlow.physicalCoefficient k D.m₀ D.T G.A ell)).forward
↑t) ∧ (∀ (t : ↑(Set.Icc 0 D.T)) (n : ℕ),
EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q
(E t).childDisplacement.toLp ⋯ n + EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q
(E t).childVelocity.toLp ⋯ n + EulerMeanClassicalWordBounds.classicalBlockSize EulerPacketParentLabelBounds.direction q
(E t).childAcceleration.toLp ⋯ n ≤ (k ^ (10 * (q + 2))) ^ (n + 1) * ↑n.factorial ^ 2) ∧ ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
‖(G.displacementField k D.m₀ ell hell t).field x‖ ≤ k ^ (-(1 / 4))
The positive-history packet at the fixed frequency constructs the actual next parent, with the same errors and the k^80 label bound.
theorem
EulerParentPacketFrames.LabelData.joined_uniform_child
{A : Parent}
(L : LabelData A)
(I : ParticleInverse A)
(H : LowBounds A)
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(m : EulerSmoothLimit.Space)
(hm : ‖m‖ = 1)
(R : U ≃ₗᵢ[ℝ] ↥(EulerTransverseFrameCoordinates.referencePlane m))
(S : Set EulerSmoothLimit.Space)
(hS : IsCompact S)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < A.T)
(J : JoinedInputs (A.meanData H) (A.transverseData m hm R S hS) τ hτ hτT (A.historyOn H m hm R S hS τ hτ hτT))
(δ : ℝ)
(hδ : 0 < δ)
(hδ1 : δ ≤ 1)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ S)
(α : ℝ)
(hα : 0 < α)
(W : ℝ)
(hW :
EulerPacketRadiusPolynomial.RadiusPrimitives J.mean J.linear J.normal
(EulerPacketCylinderField.joinedCoefficientBudget EulerPacketTerminalDatum.period (A.meanData H)
(A.transverseData m hm R S hS) ⋯ τ hτ hτT (A.historyOn H m hm R S hS τ hτ hτT) J.normal)
δ ξ W)
(hprofile : ∀ (t : ↑(Set.Icc 0 (A.transverseData m hm R S hS).T)), α * J.linear.fullProfile t ≤ W)
(k : ℝ)
(hk : EulerPacketSourceFrequency.UniversalFrequency k)
(hfrequency :
EulerPacketInitializedOutputCost.uniformConstant * W ^ EulerPacketInitializedOutputCost.uniformPower ≤ EulerPacketSourceFrequency.smallPower k)
(hKk : L.K ≤ k)
(hinv : A.ell⁻¹ ≤ k ^ (3 / 4))
(nextEll : ℝ)
(hnext : 0 < nextEll)
(hnext1 : nextEll ≤ 1)
:
∃ (hn : 1 ≤ EulerPacketSourceFrequency.truncation k) (Q :
EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯
(EulerPacketTerminalDatum.initializedCorrectionData (A.meanData H) (A.transverseData m hm R S hS) ⋯ τ hτ hτT
(A.historyOn H m hm R S hS τ hτ hτT) δ hδ ξ hs α ⋯ (EulerPacketSourceFrequency.truncation k) hn k ⋯))
(G : EulerPhysicalGraphFlowBounds.Data EulerPacketTerminalDatum.period A.T) (hgraph :
∀ (t : ↑(Set.Icc 0 A.T)) (z : EulerLiftedGradientSpace.LiftTangent),
(EulerGraphInvariantFlow.graphConstraint k m) ((G.A.field t) z) = 0),
G.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient EulerPacketTerminalDatum.period Q
(EulerPacketTerminalDatum.initializedNormalizedField (A.meanData H) (A.transverseData m hm R S hS) ⋯ τ hτ hτT
(A.historyOn H m hm R S hS τ hτ hτT) δ hδ ξ hs α (EulerPacketSourceFrequency.truncation k) k) ∧ (∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space),
‖fderiv ℝ
(EulerPacketTerminalDatum.initializedExactPhysicalVelocity (A.meanData H)
(A.transverseData m hm R S hS) ⋯ τ hτ hτT (A.historyOn H m hm R S hS τ hτ hτT) δ hδ ξ hs α ⋯
(EulerPacketSourceFrequency.truncation k) hn k ⋯ Q t (I.normalized t))
x - (α * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ m (I.normalized t x))) • ((InnerProductSpace.rankOne ℝ)
(EulerPacketPrimaryFactorization.canonicalVelocity τ hτ hτT (A.historyOn H m hm R S hS τ hτ hτT) ξ
hs (↑t) (I.normalized t x)))
(((A.transverseData m hm R S hS).normal.field t) (I.normalized t x))‖ ≤ k ^ (-(1 / 4)) ∧ ‖fderiv ℝ
(gradient
(EulerPacketTerminalDatum.initializedExactPhysicalPressure (A.meanData H)
(A.transverseData m hm R S hS) ⋯ τ hτ hτT (A.historyOn H m hm R S hS τ hτ hτT) δ hδ ξ hs α ⋯
(EulerPacketSourceFrequency.truncation k) hn k ⋯ Q t (I.normalized t)))
x - (EulerPacketPrimaryPressure.coefficient τ hτ hτT (A.historyOn H m hm R S hS τ hτ hτT) ξ hs α t
(I.normalized t x) * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ m (I.normalized t x))) • ((InnerProductSpace.rankOne ℝ) (((A.transverseData m hm R S hS).normal.field t) (I.normalized t x)))
(((A.transverseData m hm R S hS).normal.field t) (I.normalized t x))‖ ≤ k ^ (-(1 / 4))) ∧ (∀ (t : ↑(Set.Icc 0 A.T)) (x : EulerSmoothLimit.Space),
‖(G.displacementField k m A.ell ⋯ t).field x‖ ≤ k ^ (-(1 / 4))) ∧ ∃ (LC : LabelData (A.child G k m hgraph nextEll hnext hnext1)), LC.K = k ^ 80
Initial-data convergence for the very same correction witnesses used in the exact packets. No correction is chosen again for this conclusion.
@[reducible, inline]
abbrev
EulerPacketInitial.Input.correctionBudget
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
(k : ℝ)
(hk : 4 ≤ k)
(hn : 1 ≤ EulerPacketSourceFrequency.truncation k)
:
Correction budget type used in packet initial exact limit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketInitial.Input.exactInitial
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
(k : ℝ)
(hk : 4 ≤ k)
(hn : 1 ≤ EulerPacketSourceFrequency.truncation k)
(Q : A.correctionBudget k hk hn)
:
Exact initial, constructed using scale.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketInitial.Input.exactInitial_eq
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
(k : ℝ)
(hk : 4 ≤ k)
(hn : 1 ≤ EulerPacketSourceFrequency.truncation k)
(Q : A.correctionBudget k hk hn)
:
noncomputable def
EulerPacketInitial.exactPartial
{U : ℕ → Type}
[(n : ℕ) → NormedAddCommGroup (U n)]
[(n : ℕ) → InnerProductSpace ℝ (U n)]
[∀ (n : ℕ), CompleteSpace (U n)]
(A : (n : ℕ) → Input (U n))
(J : ℕ)
(X : ℝ)
(hk : ∀ (n : ℕ), 4 ≤ EulerPacketSourceScaleSequence.frequency J X n)
(hn : ∀ (n : ℕ), 1 ≤ EulerPacketSourceFrequency.truncation (EulerPacketSourceScaleSequence.frequency J X n))
(Q : (n : ℕ) → (A n).correctionBudget (EulerPacketSourceScaleSequence.frequency J X n) ⋯ ⋯)
(N : ℕ)
:
Exact partial, defined pointwise by ∑ n ∈ range N, (A n).exactInitial (frequency J X n) (hk n) (hn n) (Q n) x.
Equations
- EulerPacketInitial.exactPartial A J X hk hn Q N x = ∑ n ∈ Finset.range N, (A n).exactInitial (EulerPacketSourceScaleSequence.frequency J X n) ⋯ ⋯ (Q n) x
Instances For
theorem
EulerPacketInitial.exactPartial_eq
{U : ℕ → Type}
[(n : ℕ) → NormedAddCommGroup (U n)]
[(n : ℕ) → InnerProductSpace ℝ (U n)]
[∀ (n : ℕ), CompleteSpace (U n)]
(A : (n : ℕ) → Input (U n))
(J : ℕ)
(X : ℝ)
(hk : ∀ (n : ℕ), 4 ≤ EulerPacketSourceScaleSequence.frequency J X n)
(hn : ∀ (n : ℕ), 1 ≤ EulerPacketSourceFrequency.truncation (EulerPacketSourceScaleSequence.frequency J X n))
(Q : (n : ℕ) → (A n).correctionBudget (EulerPacketSourceScaleSequence.frequency J X n) ⋯ ⋯)
(N : ℕ)
:
theorem
EulerPacketInitial.selectedQ_initial_Hm
{U : ℕ → Type}
[(n : ℕ) → NormedAddCommGroup (U n)]
[(n : ℕ) → InnerProductSpace ℝ (U n)]
[∀ (n : ℕ), CompleteSpace (U n)]
(A : (n : ℕ) → Input (U n))
(J : ℕ)
(X : ℝ)
(hk : ∀ (n : ℕ), 4 ≤ EulerPacketSourceScaleSequence.frequency J X n)
(hn : ∀ (n : ℕ), 1 ≤ EulerPacketSourceFrequency.truncation (EulerPacketSourceScaleSequence.frequency J X n))
(Q : (n : ℕ) → (A n).correctionBudget (EulerPacketSourceScaleSequence.frequency J X n) ⋯ ⋯)
(hJ : 2 ≤ J)
(C c : ℝ)
(hC : 0 < C)
(hc : 0 ≤ c)
(p q : ℕ)
(hX : 1 ≤ X)
(hparameter : ∀ (n : ℕ), (A n).parameterSize ≤ EulerPacketUniformFrequencyScales.parameterEnvelope J C c p q X n)
(hscale : ∀ (n : ℕ), (A n).parent.ell = EulerPacketSourceScaleSequence.supportScale J X n)
(hσ : ∀ (n : ℕ), (A n).frame.sigma * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 2)
(hfrequency : ∀ (n : ℕ), (A n).frequencyGuard (EulerPacketSourceScaleSequence.frequency J X n))
(s : ℕ)
:
Filter.Tendsto
(fun (N : ℕ) =>
EulerPhysicalL2Scaling.derivativeSum s
(exactPartial A J X hk hn Q N - (initialLimit A J hJ C c hC hc p q X hX hparameter hscale hσ hk hfrequency).field))
Filter.atTop (nhds 0)
theorem
EulerPacketInitial.selectedQ_fullInitial_Hm
{U : ℕ → Type}
[(n : ℕ) → NormedAddCommGroup (U n)]
[(n : ℕ) → InnerProductSpace ℝ (U n)]
[∀ (n : ℕ), CompleteSpace (U n)]
(A : (n : ℕ) → Input (U n))
(J : ℕ)
(X : ℝ)
(hk : ∀ (n : ℕ), 4 ≤ EulerPacketSourceScaleSequence.frequency J X n)
(hn : ∀ (n : ℕ), 1 ≤ EulerPacketSourceFrequency.truncation (EulerPacketSourceScaleSequence.frequency J X n))
(Q : (n : ℕ) → (A n).correctionBudget (EulerPacketSourceScaleSequence.frequency J X n) ⋯ ⋯)
(hJ : 2 ≤ J)
(C c : ℝ)
(hC : 0 < C)
(hc : 0 ≤ c)
(p q : ℕ)
(hX : 1 ≤ X)
(hparameter : ∀ (n : ℕ), (A n).parameterSize ≤ EulerPacketUniformFrequencyScales.parameterEnvelope J C c p q X n)
(hscale : ∀ (n : ℕ), (A n).parent.ell = EulerPacketSourceScaleSequence.supportScale J X n)
(hσ : ∀ (n : ℕ), (A n).frame.sigma * EulerPacketSourceScaleChoice.scaleSequence J X n ≤ 2)
(hfrequency : ∀ (n : ℕ), (A n).frequencyGuard (EulerPacketSourceScaleSequence.frequency J X n))
(base : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space)
(s : ℕ)
:
Filter.Tendsto
(fun (N : ℕ) =>
EulerPhysicalL2Scaling.derivativeSum s
(base.field + exactPartial A J X hk hn Q N - (fullInitialLimit A J hJ C c hC hc p q X hX hparameter hscale hσ hk hfrequency base).field))
Filter.atTop (nhds 0)
structure
EulerParentPacketFrames.GeometryJoinedChoice
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(I : EulerPacketInitial.Input U)
(S : SmoothState I.parent)
(k : ℝ)
(hk : EulerPacketSourceFrequency.UniversalFrequency k)
(nextEll : ℝ)
(hnext : 0 < nextEll)
(hnext1 : nextEll ≤ 1)
:
Geometry joined choice data, collecting hn, Q, flow, graph, coefficient, labels
and their compatibility conditions.
- Q : I.correctionBudget k ⋯ ⋯
Scale parameter of
GeometryJoinedChoice, of typeI.correctionBudget k hk.four hn. Flow of
GeometryJoinedChoice, of typeEulerPhysicalGraphFlowBounds.Data period I.parent.T.- graph (t : ↑(Set.Icc 0 I.parent.T)) (q : EulerLiftedGradientSpace.LiftTangent) : (EulerGraphInvariantFlow.graphConstraint k I.normal) ((self.flow.A.field t) q) = 0
- coefficient : self.flow.A = EulerAllOrderDriftCorrection.Budget.liftedPacketCoefficient EulerPacketTerminalDatum.period self.Q (EulerPacketTerminalDatum.initializedNormalizedField I.meanData I.data ⋯ I.historyTime ⋯ ⋯ I.history I.geometry.δ ⋯ I.terminal ⋯ I.alpha (EulerPacketSourceFrequency.truncation k) k)
Label type of
GeometryJoinedChoice, of typeLabelData (I.parent.child flow k I.normal graph nextEll hnext hnext1).- errors : S.evolution.SourceErrors I.normal ⋯ I.coordinates I.support ⋯ self.Q (EulerPacketTerminalDatum.initializedApproximationResidual I.meanData I.data ⋯ I.historyTime ⋯ ⋯ I.history I.geometry.δ ⋯ I.terminal ⋯ I.alpha ⋯ (EulerPacketSourceFrequency.truncation k) ⋯ k ⋯) k I.geometry ⋯ ⋯ (k ^ (-(1 / 4))) (k ^ (-(1 / 4)))
Instances For
theorem
EulerParentPacketFrames.exists_geometryJoinedChoice
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(I : EulerPacketInitial.Input U)
(S : SmoothState I.parent)
(k : ℝ)
(hk : EulerPacketSourceFrequency.UniversalFrequency k)
(nextEll : ℝ)
(hnext : 0 < nextEll)
(hnext1 : nextEll ≤ 1)
(hterminal :
I.terminal = EulerPacketSourceGeometry.Guards.terminal ⋯ ⋯ I.frame
(I.parent.historyOn I.low I.normal ⋯ I.coordinates I.support ⋯ I.historyTime ⋯ ⋯) I.geometry)
(hfrequency : I.frequencyGuard k)
(hK : I.label.K ≤ k)
(hell : I.parent.ell⁻¹ ≤ k ^ (3 / 4))
:
Nonempty (GeometryJoinedChoice I S k hk nextEll hnext hnext1)
noncomputable def
EulerParentPacketFrames.GeometryJoinedChoice.parent
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(I : EulerPacketInitial.Input U)
(S : SmoothState I.parent)
(k : ℝ)
(hk : EulerPacketSourceFrequency.UniversalFrequency k)
(nextEll : ℝ)
(hnext : 0 < nextEll)
(hnext1 : nextEll ≤ 1)
(F : GeometryJoinedChoice I S k hk nextEll hnext hnext1)
:
Parent, given by I.parent.child F.flow k I.normal F.graph nextEll hnext hnext1.
Equations
Instances For
noncomputable def
EulerParentPacketFrames.GeometryJoinedChoice.state
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(I : EulerPacketInitial.Input U)
(S : SmoothState I.parent)
(k : ℝ)
(hk : EulerPacketSourceFrequency.UniversalFrequency k)
(nextEll : ℝ)
(hnext : 0 < nextEll)
(hnext1 : nextEll ≤ 1)
(F : GeometryJoinedChoice I S k hk nextEll hnext hnext1)
(hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support)
:
SmoothState (parent I S k hk nextEll hnext hnext1 F)
State, constructed using S.joinedChild.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerParentPacketFrames.GeometryJoinedChoice.state_label_constant
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(I : EulerPacketInitial.Input U)
(S : SmoothState I.parent)
(k : ℝ)
(hk : EulerPacketSourceFrequency.UniversalFrequency k)
(nextEll : ℝ)
(hnext : 0 < nextEll)
(hnext1 : nextEll ≤ 1)
(F : GeometryJoinedChoice I S k hk nextEll hnext hnext1)
(hSym : ∀ (x : EulerSmoothLimit.Space), -x ∈ I.support ↔ x ∈ I.support)
:
theorem
EulerParentPacketFrames.GeometryJoinedChoice.initial_trace
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(I : EulerPacketInitial.Input U)
(S : SmoothState I.parent)
(k : ℝ)
(hk : EulerPacketSourceFrequency.UniversalFrequency k)
(nextEll : ℝ)
(hnext : 0 < nextEll)
(hnext1 : nextEll ≤ 1)
(F : GeometryJoinedChoice I S k hk nextEll hnext hnext1)
: