Genuine parent/geometry inputs for an initial increment. The high and mean fields below are the actual solved profiles, not prescribed bounds.
The high initial increment retains its small amplitude, while the mean initial increment is O(k⁻²) without any oscillatory-graph loss.
Initial high and mean estimates retain their distinct small factors. The only truncation-dependent quantity is the already controlled tail base.
theorem
EulerPacketCylinderField.Field.wordBound_evaluate_low_high_scaled
{P T : ℝ}
[Fact (0 < P)]
(N : ℕ)
(hN : 1 ≤ N)
(κ B C₁ C₂ γ : ℝ)
(hκ : 0 ≤ κ)
(hB : 0 ≤ B)
(hγ : 0 < γ)
(hsmall : κ * B ≤ 1 / 2)
(f : ℕ → EulerPacketProfileRecursion.VectorField)
(H : (i : ℕ) → Field P T (f i))
(q : ℕ)
(R : ℝ)
(hR : 0 ≤ R)
(hzero : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), f 0 (↑t, x, θ) = 0)
(hone : (H 1).WordBound q R (γ * C₁) 0)
(htwo : (H 2).WordBound q R (γ * C₂) 0)
(htail : ∀ (n : ℕ), 3 ≤ n → n ≤ N + 1 → (H n).WordBound q R (γ * B ^ (n + 1)) 0)
:
theorem
EulerPacketInitial.highGrade_bound
{P T : ℝ}
[Fact (0 < P)]
{hT : 0 ≤ T}
{N : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{support : Set EulerSmoothLimit.Space}
(G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T hT support (a i))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T))
(R : ℝ)
(hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → EulerPacketCylinderField.ProfileBudget (G i hi) S R i)
(hR : 1 ≤ R)
(ha : a 0 = 0)
(t : ↑(Set.Icc 0 T))
(n : ℕ)
:
(highGradeField G t n).WordBound 6 R (S.growth t * (3 * S.H0 ^ (2 * n))) (EulerPacketShiftArithmetic.highShift n)
theorem
EulerPacketInitial.meanGrade_bound
{P T : ℝ}
[Fact (0 < P)]
{hT : 0 ≤ T}
{N : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{support : Set EulerSmoothLimit.Space}
(G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T hT support (a i))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T))
(R : ℝ)
(hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → EulerPacketCylinderField.ProfileBudget (G i hi) S R i)
(hR : 1 ≤ R)
(ha : a 0 = 0)
(t : ↑(Set.Icc 0 T))
(n : ℕ)
:
(meanGradeField G t n).WordBound 6 R (3 * S.H0 ^ (2 * n)) (EulerPacketShiftArithmetic.highShift n)
theorem
EulerPacketInitial.high_bound
{P T : ℝ}
[Fact (0 < P)]
{hT : 0 ≤ T}
{N : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{support : Set EulerSmoothLimit.Space}
(G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T hT support (a i))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T))
(R : ℝ)
(hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → EulerPacketCylinderField.ProfileBudget (G i hi) S R i)
(hR : 1 ≤ R)
(ha : a 0 = 0)
(t : ↑(Set.Icc 0 T))
(hN : 1 ≤ N)
(C κ : ℝ)
(hC : 1 ≤ C)
(hκ : 0 ≤ κ)
(hsmall : κ * EulerPacketCoarseMajorant.tailBase R S.H0 C N ≤ 1 / 2)
:
theorem
EulerPacketInitial.mean_bound
{P T : ℝ}
[Fact (0 < P)]
{hT : 0 ≤ T}
{N : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{support : Set EulerSmoothLimit.Space}
(G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T hT support (a i))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T))
(R : ℝ)
(hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → EulerPacketCylinderField.ProfileBudget (G i hi) S R i)
(hR : 1 ≤ R)
(ha : a 0 = 0)
(t : ↑(Set.Icc 0 T))
(hN : 1 ≤ N)
(ha1 : (a 1).mean = 0)
(C κ : ℝ)
(hC : 1 ≤ C)
(hκ : 0 ≤ κ)
(hsmall : κ * EulerPacketCoarseMajorant.tailBase R S.H0 C N ≤ 1 / 2)
:
High cost, given by fixedVelocityGradeCost R H 1+fixedVelocityGradeCost R H 2+1.
Equations
Instances For
Mean cost, given by fixedVelocityGradeCost R H 2+2.
Equations
Instances For
theorem
EulerPacketInitial.high_frequency_bound
{P T : ℝ}
[Fact (0 < P)]
{hT : 0 ≤ T}
{N : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{support : Set EulerSmoothLimit.Space}
(G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T hT support (a i))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T))
(R : ℝ)
(hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → EulerPacketCylinderField.ProfileBudget (G i hi) S R i)
(hR : 1 ≤ R)
(ha : a 0 = 0)
(t : ↑(Set.Icc 0 T))
(hN : 1 ≤ N)
(C k : ℝ)
(hC : 1 ≤ C)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase R S.H0 C N ≤ k ^ (1 / 100))
:
theorem
EulerPacketInitial.mean_frequency_bound
{P T : ℝ}
[Fact (0 < P)]
{hT : 0 ≤ T}
{N : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{support : Set EulerSmoothLimit.Space}
(G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T hT support (a i))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T))
(R : ℝ)
(hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → EulerPacketCylinderField.ProfileBudget (G i hi) S R i)
(hR : 1 ≤ R)
(ha : a 0 = 0)
(t : ↑(Set.Icc 0 T))
(hN : 1 ≤ N)
(C k : ℝ)
(hC : 1 ≤ C)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase R S.H0 C N ≤ k ^ (1 / 100))
(ha1 : (a 1).mean = 0)
:
theorem
EulerPacketInitial.high_physical_bound
{P T : ℝ}
[Fact (0 < P)]
{hT : 0 ≤ T}
{N : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{support : Set EulerSmoothLimit.Space}
(G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T hT support (a i))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T))
(R : ℝ)
(hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → EulerPacketCylinderField.ProfileBudget (G i hi) S R i)
(hR : 1 ≤ R)
(ha : a 0 = 0)
(t : ↑(Set.Icc 0 T))
(hN : 1 ≤ N)
(C k : ℝ)
(hC : 1 ≤ C)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase R S.H0 C N ≤ k ^ (1 / 100))
(ell : ℝ)
(hell : 0 < ell)
(hell1 : ell ≤ 1)
(m : EulerSmoothLimit.Space)
(s : ℕ)
:
EulerPhysicalL2Scaling.derivativeSum s
(EulerPhysicalL2Scaling.scale ell fun (x : EulerSmoothLimit.Space) => high N k⁻¹ (↑t) a (↑t, x, k * inner ℝ m x)) ≤ ell⁻¹ ^ s * k ^ s * S.growth t * (highCost R S.H0 * EulerPhysicalL2Scaling.physicalDerivativeCost P (4 * R)
(‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * (1 + ‖m‖)) s)
theorem
EulerPacketInitial.mean_physical_bound
{P T : ℝ}
[Fact (0 < P)]
{hT : 0 ≤ T}
{N : ℕ}
{a : ℕ → EulerPacketProfileRecursion.Profile}
{support : Set EulerSmoothLimit.Space}
(G : (i : ℕ) → i ≤ N → EulerPacketCylinderField.ProfileRegularity P T hT support (a i))
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 T))
(R : ℝ)
(hG : ∀ (i : ℕ) (hi : i ≤ N), 1 ≤ i → EulerPacketCylinderField.ProfileBudget (G i hi) S R i)
(hR : 1 ≤ R)
(ha : a 0 = 0)
(t : ↑(Set.Icc 0 T))
(hN : 1 ≤ N)
(C k : ℝ)
(hC : 1 ≤ C)
(hk : 4 ≤ k)
(hbase : EulerPacketCoarseMajorant.tailBase R S.H0 C N ≤ k ^ (1 / 100))
(ha1 : (a 1).mean = 0)
(ell : ℝ)
(hell : 0 < ell)
(hell1 : ell ≤ 1)
(m : EulerSmoothLimit.Space)
(s : ℕ)
:
EulerPhysicalL2Scaling.derivativeSum s
(EulerPhysicalL2Scaling.scale ell fun (x : EulerSmoothLimit.Space) => mean N k⁻¹ (↑t) a (↑t, x, k * inner ℝ m x)) ≤ ell⁻¹ ^ s / k ^ 2 * (meanCost R S.H0 * EulerPhysicalL2Scaling.physicalDerivativeCost P (4 * R) ‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ s)
Source (22) for the literal initialized packet. The constants at each fixed Sobolev order are independent of its truncation and frequency.
noncomputable def
EulerPacketTerminalDatum.initializedInitialHigh
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(k : ℝ)
:
Initialized initial high, given by scale M.ℓ (fun x => EulerPacketInitial.high N k⁻¹ 0 (initializedProfiles M D τ hτ hτT B δ hδ ξ hs α) (0,(x,k*inner ℝ D.m₀ x))).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketTerminalDatum.initializedInitialMean
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(k : ℝ)
:
Initialized initial mean, given by scale M.ℓ (fun x => EulerPacketInitial.mean N k⁻¹ 0 (initializedProfiles M D τ hτ hτT B δ hδ ξ hs α) (0,(x,k*inner ℝ D.m₀ x))).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.initializedInitialHigh_support
(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)
(α : ℝ)
(hS : D.support ⊆ Metric.closedBall 0 (1 / 2))
(N : ℕ)
(k : ℝ)
:
tsupport (initializedInitialHigh M D τ hτ hτT B δ hδ ξ hs α N k) ⊆ Metric.closedBall 0 (M.ℓ / 2)
theorem
EulerPacketTerminalDatum.initializedInitialMean_support
(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 : ℝ)
:
tsupport (initializedInitialMean M D τ hτ hτT B δ hδ ξ hs α N k) ⊆ Metric.closedBall 0 2
theorem
EulerPacketTerminalDatum.initializedInitial_common_support
(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)
(α : ℝ)
(hS : D.support ⊆ Metric.closedBall 0 (1 / 2))
(N : ℕ)
(k : ℝ)
:
tsupport (initializedInitialHigh M D τ hτ hτT B δ hδ ξ hs α N k) ⊆ Metric.closedBall 0 2 ∧ tsupport (initializedInitialMean M D τ hτ hτT B δ hδ ξ hs α N k) ⊆ Metric.closedBall 0 2
theorem
EulerPacketTerminalDatum.initializedInitialMean_zero
(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)
(α : ℝ)
(hL : M.L = 0)
(N : ℕ)
(k : ℝ)
:
theorem
EulerPacketTerminalDatum.initialized_growth_initial
(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τ ⋯))
(α : ℝ)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT B (Fin 4) 6)
(S : EulerPacketTimeProfile.Scales ↑(Set.Icc 0 M.T))
(hgrowth : EulerPacketCylinderField.timeProfileChange S.growth hTime = α • L.fullProfile)
:
theorem
EulerPacketTerminalDatum.initializedInitialHigh_Hm
(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))
(s : ℕ)
:
theorem
EulerPacketTerminalDatum.initializedInitialMean_Hm
(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))
(s : ℕ)
:
EulerPhysicalL2Scaling.derivativeSum s (initializedInitialMean M D τ hτ hτT B δ hδ ξ hs α N k) ≤ M.ℓ⁻¹ ^ s / k ^ 2 * (EulerPacketInitial.meanCost L.R S.H0 * EulerPhysicalL2Scaling.physicalDerivativeCost period (4 * L.R) ‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ s)
The actual chosen primary amplitude has exponential initial decay. Its prefactor is a fixed polynomial in the same source parameters.
Envelope, given by 4*X^2*(1+sourceEnvelope X).
Equations
Instances For
Polynomial, given by 4*Polynomial.X^2*(1+sourcePolynomial).
Equations
Instances For
Degree, given by polynomial.natDegree.
Instances For
theorem
EulerPacketSourceGeometry.Guards.primaryAmplitude_polynomial
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{τ : ℝ}
{hτ : 0 < τ}
{hτT : τ < D.T}
{P : ParentFrame D τ}
{H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)}
(J : Guards hτ hτT P H)
(hball : 1 / 2 ≤ J.radius)
(L : EulerTransversePacketJoin.Budget D τ hτ hτT H (Fin 4) 6)
(X x : ℝ)
(hX : 1 ≤ X)
(hH : P.horizon ≤ X)
(hh : J.hchild ≤ X)
(hδ : J.δ ≤ 1)
(hC : L.C₀ ≤ EulerParentInitializedRadius.sourceEnvelope X)
(hσ : P.sigma * x ≤ 2)
:
theorem
EulerPacketSourceGeometry.Guards.horizon_le_growthCost
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
{D : EulerTransversePacketProvider.Data U}
{τ : ℝ}
{hτ : 0 < τ}
{hτT : τ < D.T}
{P : ParentFrame D τ}
{H : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯)}
(J : Guards hτ hτT P H)
:
theorem
EulerPacketSourceGeometry.ForwardGuards.primaryAmplitude_polynomial
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{P : ParentFrame D 0}
(J : ForwardGuards P)
(hball : 1 / 2 ≤ J.radius)
(X x : ℝ)
(hX : 1 ≤ X)
(hH : P.horizon ≤ X)
(hh : J.hchild ≤ X)
(hδ : J.δ ≤ 1)
(hσ : P.sigma * x ≤ 2)
:
theorem
EulerPacketSourceGeometry.ForwardGuards.horizon_le_growthCost
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{P : ParentFrame D 0}
(J : ForwardGuards P)
(hball : 1 / 2 ≤ J.radius)
:
At each fixed Sobolev order, the two actual initial-increment costs are fixed polynomials in the source primitives. Frequency and amplitude are kept outside these polynomials.
Jet polynomial map, given by ∑ n ∈ range (s+1), R^n*Polynomial.C ((n.factorial : ℝ)^2).
Equations
- EulerPacketInitialCost.jetPolynomialMap R s = ∑ n ∈ Finset.range (s + 1), R ^ n * Polynomial.C (↑n.factorial ^ 2)
Instances For
Physical polynomial, given by ∑ n ∈ range (s+1), Polynomial.C ((4*C)^n*Real.sqrt (2/period+2*period)) * jetPolynomialMap R (n+1).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Polynomial, given by 1+(gradePolynomial 1+2*gradePolynomial 2+3) * physicalPolynomial (4*Polynomial.X) (coordinateCost*2) s.
Instances For
theorem
EulerPacketInitialCost.costs_le_envelope
(s : ℕ)
(R H X : ℝ)
(hR : 0 ≤ R)
(hH : 0 ≤ H)
(hRX : R ≤ X)
(hHX : H ≤ X)
:
EulerPacketInitial.highCost R H * EulerPhysicalL2Scaling.physicalDerivativeCost EulerPacketTerminalDatum.period (4 * R)
(EulerPacketPhysicalCost.coordinateCost * 2) s ≤ envelope s X ∧ EulerPacketInitial.meanCost R H * EulerPhysicalL2Scaling.physicalDerivativeCost EulerPacketTerminalDatum.period (4 * R)
EulerPacketPhysicalCost.coordinateCost s ≤ envelope s X
Source polynomial as an element of Polynomial ℝ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Source constant, given by coefficientCost (sourcePolynomial s).
Equations
Instances For
Source power, given by (sourcePolynomial s).natDegree.
Equations
Instances For
The exact correction has zero initial value, so the two actual compactly supported initial increments are precisely the finite-packet high and mean fields whose physical Sobolev bounds were proved above.
theorem
EulerPacketTerminalDatum.initializedInitial_split
(M : EulerMeanPacketProvider.Data)
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(α : ℝ)
(N : ℕ)
(k : ℝ)
:
(EulerPhysicalL2Scaling.scale M.ℓ fun (x : EulerSmoothLimit.Space) =>
initializedVelocity M D τ hτ hτT B δ hδ ξ hs α N k⁻¹ (0, x, k * inner ℝ D.m₀ x)) = initializedInitialHigh M D τ hτ hτT B δ hδ ξ hs α N k + initializedInitialMean M D τ hτ hτT B δ hδ ξ hs α N k
theorem
EulerPacketTerminalDatum.initializedInitialHigh_memLp
(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 n : ℕ)
(k : ℝ)
:
MeasureTheory.MemLp (iteratedFDeriv ℝ n (initializedInitialHigh M D τ hτ hτT B δ hδ ξ hs α N k)) 2 MeasureTheory.volume
theorem
EulerPacketTerminalDatum.initializedInitialMean_memLp
(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 n : ℕ)
(k : ℝ)
:
MeasureTheory.MemLp (iteratedFDeriv ℝ n (initializedInitialMean M D τ hτ hτT B δ hδ ξ hs α N k)) 2 MeasureTheory.volume
theorem
EulerPacketTerminalDatum.initializedInitial_compact
(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)
(α : ℝ)
(hS : D.support ⊆ Metric.closedBall 0 (1 / 2))
(N : ℕ)
(k : ℝ)
:
HasCompactSupport (initializedInitialHigh M D τ hτ hτT B δ hδ ξ hs α N k) ∧ HasCompactSupport (initializedInitialMean M D τ hτ hτT B δ hδ ξ hs α N k)
theorem
EulerPacketTerminalDatum.initializedExactPhysicalVelocity_initial
(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)
(α : ℝ)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(Q :
EulerAllOrderDriftCorrection.Budget period ⋯
(initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk))
(x : EulerSmoothLimit.Space)
:
theorem
EulerPacketTerminalDatum.initializedExactPhysicalVelocity_initial_split
(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)
(α : ℝ)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(N : ℕ)
(hN : 1 ≤ N)
(k : ℝ)
(hk : 4 ≤ k)
(Q :
EulerAllOrderDriftCorrection.Budget period ⋯
(initializedCorrectionData M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk))
:
EulerPhysicalL2Scaling.scale M.ℓ
(initializedExactPhysicalVelocity M D hTime τ hτ hτT B δ hδ ξ hs α Cagree N hN k hk Q ⟨0, ⋯⟩ id) = initializedInitialHigh M D τ hτ hτT B δ hδ ξ hs α N k + initializedInitialMean M D τ hτ hτT B δ hδ ξ hs α N k
Source-only initial estimates for the actual packet constructed from a parent and its activation geometry. No initial-field estimate is an input.
The actual initial increments for the canonical uniformly selected packet satisfy source (22), with fixed-order polynomial costs.
theorem
EulerPacketTerminalDatum.initialized_uniform_initial_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)
(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)
(hfrequency :
EulerPacketInitializedCost.uniformConstant * W ^ EulerPacketInitializedCost.uniformPower ≤ EulerPacketSourceFrequency.smallPower k)
(s : ℕ)
:
EulerPhysicalL2Scaling.derivativeSum s
(initializedInitialHigh M D τ hτ hτT B δ hδ ξ hs α (EulerPacketSourceFrequency.truncation k) k) ≤ M.ℓ⁻¹ ^ s * k ^ s * α * EulerPacketInitialCost.envelope s (EulerPacketInitializedCost.envelope W) ∧ EulerPhysicalL2Scaling.derivativeSum s
(initializedInitialMean M D τ hτ hτT B δ hδ ξ hs α (EulerPacketSourceFrequency.truncation k) k) ≤ M.ℓ⁻¹ ^ s / k ^ 2 * EulerPacketInitialCost.envelope s (EulerPacketInitializedCost.envelope W)
theorem
EulerPacketTerminalDatum.initializedUniformBudget_initial
(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)
(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)
(hfrequency :
EulerPacketInitializedCost.uniformConstant * W ^ EulerPacketInitializedCost.uniformPower ≤ EulerPacketSourceFrequency.smallPower k)
(Cagree : EulerPacketCylinderField.SourceCoefficientAgreement M D)
(hX : 64 ≤ EulerPacketSourceFrequency.expansion k)
(hlog : 1 ≤ Real.log k)
(Ξ : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(hΞ : ∀ (t : ↑(Set.Icc 0 D.T)), ContDiff ℝ (↑⊤) (Ξ t))
(hF : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), fderiv ℝ (Ξ t) x = (D.F.field t) x)
(hdet :
∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1)
(s : ℕ)
:
EulerPhysicalL2Scaling.scale M.ℓ
(initializedExactPhysicalVelocity M D hTime τ hτ hτT B δ hδ ξ hs α Cagree
(EulerPacketSourceFrequency.truncation k) ⋯ k hk
(initializedUniformBudget M D hTime τ hτ hτT B δ hδ hδ1 ξ hs α hα L NB LM Cagree W hW hprofile k hk hX hlog
hfrequency Ξ hΞ hF hdet)
⟨0, ⋯⟩ id) = initializedInitialHigh M D τ hτ hτT B δ hδ ξ hs α (EulerPacketSourceFrequency.truncation k) k + initializedInitialMean M D τ hτ hτT B δ hδ ξ hs α (EulerPacketSourceFrequency.truncation k) k ∧ EulerPhysicalL2Scaling.derivativeSum s
(initializedInitialHigh M D τ hτ hτT B δ hδ ξ hs α (EulerPacketSourceFrequency.truncation k) k) ≤ M.ℓ⁻¹ ^ s * k ^ s * α * EulerPacketInitialCost.envelope s (EulerPacketInitializedCost.envelope W) ∧ EulerPhysicalL2Scaling.derivativeSum s
(initializedInitialMean M D τ hτ hτT B δ hδ ξ hs α (EulerPacketSourceFrequency.truncation k) k) ≤ M.ℓ⁻¹ ^ s / k ^ 2 * EulerPacketInitialCost.envelope s (EulerPacketInitializedCost.envelope W)
Fixed-order source polynomial bounds for the literal initial increments. These use the same finite frequency guard as the constructed exact packet.
theorem
EulerPacketUniformSource.initial_frequency_guard
(X k : ℝ)
(hX : 1 ≤ X)
(h : frequencyConstant * X ^ frequencyPower ≤ EulerPacketSourceFrequency.smallPower k)
:
theorem
EulerPacketTerminalDatum.initialized_initial_polynomial_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)
(X : ℝ)
(hX : 1 ≤ X)
(hW :
EulerPacketRadiusPolynomial.RadiusPrimitives LM L NB
(EulerPacketCylinderField.joinedCoefficientBudget period M D hTime τ hτ hτT B NB) δ ξ
(EulerPacketUniformSource.profileEnvelope X))
(hprofile : ∀ (t : ↑(Set.Icc 0 D.T)), α * L.fullProfile t ≤ EulerPacketUniformSource.profileEnvelope X)
(k : ℝ)
(hk : 4 ≤ k)
(hfrequency :
EulerPacketUniformSource.frequencyConstant * X ^ EulerPacketUniformSource.frequencyPower ≤ EulerPacketSourceFrequency.smallPower k)
(s : ℕ)
:
EulerPhysicalL2Scaling.derivativeSum s
(initializedInitialHigh M D τ hτ hτT B δ hδ ξ hs α (EulerPacketSourceFrequency.truncation k) k) ≤ M.ℓ⁻¹ ^ s * k ^ s * α * (EulerPacketInitialCost.sourceConstant s * X ^ EulerPacketInitialCost.sourcePower s) ∧ EulerPhysicalL2Scaling.derivativeSum s
(initializedInitialMean M D τ hτ hτT B δ hδ ξ hs α (EulerPacketSourceFrequency.truncation k) k) ≤ M.ℓ⁻¹ ^ s / k ^ 2 * (EulerPacketInitialCost.sourceConstant s * X ^ EulerPacketInitialCost.sourcePower s)
theorem
EulerParentPacketFrames.LabelData.geometry_initial_primitives
{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)
(P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) τ)
(J : EulerPacketSourceGeometry.Guards hτ hτT P (G.historyOn H m hm R S hS τ hτ hτT))
(hball : 1 / 2 ≤ J.radius)
(Ti TiTotal : ℝ)
(hτ1 : τ ≤ 1)
(hTi : τ⁻¹ ≤ Ti)
(hT1 : G.T ≤ 1)
(hTiTotal : G.T⁻¹ ≤ TiTotal)
(Ω : Set EulerSmoothLimit.Space)
(hΩ : MeasurableSet Ω)
(hΩo : IsOpen Ω)
(hsub : S ⊆ Ω)
(hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2)
(ξ : U)
(hδ : 0 < J.δ)
:
have X := L.geometryParameterSize H m hm R S hS τ hτ hτT P J Ti TiTotal ξ;
1 ≤ X ∧ P.horizon ≤ X ∧ J.hchild ≤ X ∧ EulerPacketRadiusPolynomial.RadiusPrimitives
(L.geometryInputs H m hm R S hS τ hτ hτT P J hball Ti TiTotal hτ1 hTi hT1 hTiTotal Ω hΩ hΩo hsub hΩball).mean
(L.geometryInputs H m hm R S hS τ hτ hτT P J hball Ti TiTotal hτ1 hTi hT1 hTiTotal Ω hΩ hΩo hsub hΩball).linear
(L.geometryInputs H m hm R S hS τ hτ hτT P J hball Ti TiTotal hτ1 hTi hT1 hTiTotal Ω hΩ hΩo hsub hΩball).normal
(EulerPacketCylinderField.joinedCoefficientBudget EulerPacketTerminalDatum.period (G.meanData H)
(G.transverseData m hm R S hS) ⋯ τ hτ hτT (G.historyOn H m hm R S hS τ hτ hτT)
(L.geometryInputs H m hm R S hS τ hτ hτT P J hball Ti TiTotal hτ1 hTi hT1 hTiTotal Ω hΩ hΩo hsub
hΩball).normal)
J.δ ξ (EulerParentInitializedRadius.sourceEnvelope X)
theorem
EulerParentPacketFrames.LabelData.geometry_initial_amplitude
{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)
(P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) τ)
(J : EulerPacketSourceGeometry.Guards hτ hτT P (G.historyOn H m hm R S hS τ hτ hτT))
(hball : 1 / 2 ≤ J.radius)
(Ti TiTotal : ℝ)
(hτ1 : τ ≤ 1)
(hTi : τ⁻¹ ≤ Ti)
(hT1 : G.T ≤ 1)
(hTiTotal : G.T⁻¹ ≤ TiTotal)
(Ω : Set EulerSmoothLimit.Space)
(hΩ : MeasurableSet Ω)
(hΩo : IsOpen Ω)
(hsub : S ⊆ Ω)
(hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2)
(ξ : U)
(hδ : 0 < J.δ)
(hδ1 : J.δ ≤ 1)
(x : ℝ)
(hσ : P.sigma * x ≤ 2)
:
have X := L.geometryParameterSize H m hm R S hS τ hτ hτT P J Ti TiTotal ξ;
J.primaryAmplitude hball ≤ EulerPacketInitialAmplitude.boundConstant * X ^ EulerPacketInitialAmplitude.degree * Real.exp (-x / 8)
theorem
EulerParentPacketFrames.LabelData.geometry_initial_bounds
{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)
(P : EulerPacketSourceGeometry.ParentFrame (G.transverseData m hm R S hS) τ)
(J : EulerPacketSourceGeometry.Guards hτ hτT P (G.historyOn H m hm R S hS τ hτ hτT))
(hball : 1 / 2 ≤ J.radius)
(Ti TiTotal : ℝ)
(hτ1 : τ ≤ 1)
(hTi : τ⁻¹ ≤ Ti)
(hT1 : G.T ≤ 1)
(hTiTotal : G.T⁻¹ ≤ TiTotal)
(Ω : Set EulerSmoothLimit.Space)
(hΩ : MeasurableSet Ω)
(hΩo : IsOpen Ω)
(hsub : S ⊆ Ω)
(hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ S)
(hδ : 0 < J.δ)
(hδ1 : J.δ ≤ 1)
(hh : 0 < J.hchild)
(x : ℝ)
(hσ : P.sigma * x ≤ 2)
(k : ℝ)
(hk : 4 ≤ k)
(hfrequency :
EulerPacketUniformSource.frequencyConstant * L.geometryParameterSize H m hm R S hS τ hτ hτT P J Ti TiTotal ξ ^ EulerPacketUniformSource.frequencyPower ≤ EulerPacketSourceFrequency.smallPower k)
(s : ℕ)
:
have X := L.geometryParameterSize H m hm R S hS τ hτ hτT P J Ti TiTotal ξ;
EulerPhysicalL2Scaling.derivativeSum s
(EulerPacketTerminalDatum.initializedInitialHigh (G.meanData H) (G.transverseData m hm R S hS) τ hτ hτT
(G.historyOn H m hm R S hS τ hτ hτT) J.δ hδ ξ hs (J.primaryAmplitude hball)
(EulerPacketSourceFrequency.truncation k) k) ≤ G.ell⁻¹ ^ s * k ^ s * (EulerPacketInitialAmplitude.boundConstant * EulerPacketInitialCost.sourceConstant s * X ^ (EulerPacketInitialAmplitude.degree + EulerPacketInitialCost.sourcePower s)) * Real.exp (-x / 8) ∧ EulerPhysicalL2Scaling.derivativeSum s
(EulerPacketTerminalDatum.initializedInitialMean (G.meanData H) (G.transverseData m hm R S hS) τ hτ hτT
(G.historyOn H m hm R S hS τ hτ hτT) J.δ hδ ξ hs (J.primaryAmplitude hball)
(EulerPacketSourceFrequency.truncation k) k) ≤ G.ell⁻¹ ^ s / k ^ 2 * (EulerPacketInitialCost.sourceConstant s * X ^ EulerPacketInitialCost.sourcePower s)
Ordinary smooth square-integrable fields realizing both actual initial increments, with the same concrete high and mean functions.
noncomputable def
EulerPacketTerminalDatum.initializedInitialHighField
(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 : ℝ)
:
Initialized initial high field, bundling field, smooth, let, integrable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketTerminalDatum.initializedInitialMeanField
(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 : ℝ)
:
Initialized initial mean field, bundling field, smooth, let, integrable.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketTerminalDatum.initializedInitialHighField_field
(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 : ℝ)
:
(initializedInitialHighField M D hTime τ hτ hτT B δ hδ ξ hs α N k).field = initializedInitialHigh M D τ hτ hτT B δ hδ ξ hs α N k
theorem
EulerPacketTerminalDatum.initializedInitialMeanField_field
(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 : ℝ)
:
(initializedInitialMeanField M D hTime τ hτ hτT B δ hδ ξ hs α N k).field = initializedInitialMean M D τ hτ hτT B δ hδ ξ hs α N k
structure
EulerPacketInitial.Input
(U : Type)
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
:
Input data, collecting parent, label, low, normal, normal_unit, coordinates and
their compatibility conditions.
- parent : EulerParentPacketFrames.Parent
Parent of
Input, of typeParent. - label : EulerParentPacketFrames.LabelData self.parent
- low : EulerParentPacketFrames.LowBounds self.parent
- normal : EulerSmoothLimit.Space
Normal of
Input, of typeSpace. Coordinates of
Input, of typeU ≃ₗᵢ[ℝ] EulerTransverseFrameCoordinates.referencePlane normal.- support : Set EulerSmoothLimit.Space
- historyTime : ℝ
History time of
Input, of typeℝ. - frame : EulerPacketSourceGeometry.ParentFrame (self.parent.transverseData self.normal ⋯ self.coordinates self.support ⋯) self.historyTime
Frame supplied by
Input. - geometry : EulerPacketSourceGeometry.Guards ⋯ ⋯ self.frame (self.parent.historyOn self.low self.normal ⋯ self.coordinates self.support ⋯ self.historyTime ⋯ ⋯)
Geometry supplied by
Input. - neighborhood : Set EulerSmoothLimit.Space
- neighborhood_measurable : MeasurableSet self.neighborhood
- neighborhood_open : IsOpen self.neighborhood
- support_subset : self.support ⊆ self.neighborhood
- neighborhood_bound (x : EulerSmoothLimit.Space) : x ∈ self.neighborhood → ‖x‖ ≤ 1 / 2
- terminal : U
Terminal of
Input, of typeU. - cutoff_support : tsupport EulerSpatialCutoffs.innerCutoff ⊆ self.support
Instances For
@[reducible, inline]
noncomputable abbrev
EulerPacketInitial.Input.data
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
:
Data: an abbreviation for A.parent.transverseData A.normal A.normal_unit A.coordinates A.support A.support_compact.
Equations
- A.data = A.parent.transverseData A.normal ⋯ A.coordinates A.support ⋯
Instances For
@[reducible, inline]
noncomputable abbrev
EulerPacketInitial.Input.meanData
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
:
Mean data: an abbreviation for A.parent.meanData A.low.
Instances For
@[reducible, inline]
noncomputable abbrev
EulerPacketInitial.Input.history
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
:
History: an abbreviation for A.parent.historyOn A.low A.normal A.normal_unit A.coordinates A.support A.support_compact A.historyTime A.history_pos A.history_lt.
Equations
- A.history = A.parent.historyOn A.low A.normal ⋯ A.coordinates A.support ⋯ A.historyTime ⋯ ⋯
Instances For
noncomputable def
EulerPacketInitial.Input.parameterSize
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
:
Parameter size, constructed using A.label.geometryParameterSize.
Equations
- A.parameterSize = A.label.geometryParameterSize A.low A.normal ⋯ A.coordinates A.support ⋯ A.historyTime ⋯ ⋯ A.frame A.geometry A.historyTime⁻¹ A.parent.T⁻¹ A.terminal
Instances For
noncomputable def
EulerPacketInitial.Input.alpha
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
:
Alpha, given by A.geometry.primaryAmplitude A.halfBall.
Equations
- A.alpha = A.geometry.primaryAmplitude ⋯
Instances For
theorem
EulerPacketInitial.Input.alpha_pos
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
:
def
EulerPacketInitial.Input.frequencyGuard
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
(k : ℝ)
:
Frequency guard, given by frequencyConstant*A.parameterSize^frequencyPower ≤ smallPower k.
Equations
Instances For
noncomputable def
EulerPacketInitial.Input.high
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
(k : ℝ)
:
High, constructed using initializedInitialHigh.
Equations
- A.high k = EulerPacketTerminalDatum.initializedInitialHigh A.meanData A.data A.historyTime ⋯ ⋯ A.history A.geometry.δ ⋯ A.terminal ⋯ A.alpha (EulerPacketSourceFrequency.truncation k) k
Instances For
noncomputable def
EulerPacketInitial.Input.mean
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
(k : ℝ)
:
Mean, constructed using initializedInitialMean.
Equations
- A.mean k = EulerPacketTerminalDatum.initializedInitialMean A.meanData A.data A.historyTime ⋯ ⋯ A.history A.geometry.δ ⋯ A.terminal ⋯ A.alpha (EulerPacketSourceFrequency.truncation k) k
Instances For
noncomputable def
EulerPacketInitial.Input.highField
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
(k : ℝ)
:
High field, constructed using initializedInitialHighField.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerPacketInitial.Input.meanField
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
(k : ℝ)
:
Mean field, constructed using initializedInitialMeanField.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerPacketInitial.Input.highField_field
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
(k : ℝ)
:
theorem
EulerPacketInitial.Input.meanField_field
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
(k : ℝ)
:
theorem
EulerPacketInitial.Input.parameterSize_one
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
:
theorem
EulerPacketInitial.Input.initial_bounds
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
(x : ℝ)
(hσ : A.frame.sigma * x ≤ 2)
(k : ℝ)
(hk : 4 ≤ k)
(hfrequency : A.frequencyGuard k)
(s : ℕ)
:
EulerPhysicalL2Scaling.derivativeSum s (A.high k) ≤ A.parent.ell⁻¹ ^ s * k ^ s * (EulerPacketInitialAmplitude.boundConstant * EulerPacketInitialCost.sourceConstant s * A.parameterSize ^ (EulerPacketInitialAmplitude.degree + EulerPacketInitialCost.sourcePower s)) * Real.exp (-x / 8) ∧ EulerPhysicalL2Scaling.derivativeSum s (A.mean k) ≤ A.parent.ell⁻¹ ^ s / k ^ 2 * (EulerPacketInitialCost.sourceConstant s * A.parameterSize ^ EulerPacketInitialCost.sourcePower s)
theorem
EulerPacketInitial.Input.initial_support
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
(k : ℝ)
:
@[reducible, inline]
abbrev
EulerPacketInitial.Input.agreement
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
:
Agreement: an abbreviation for A.parent.sourceAgreement A.normal A.normal_unit A.coordinates A.support A.support_compact A.low.
Equations
- ⋯ = ⋯
Instances For
theorem
EulerPacketInitial.Input.sameQ_initial
{U : Type}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(A : Input U)
(k : ℝ)
(hk : 4 ≤ k)
(hn : 1 ≤ EulerPacketSourceFrequency.truncation k)
(Q :
EulerAllOrderDriftCorrection.Budget EulerPacketTerminalDatum.period ⋯
(EulerPacketTerminalDatum.initializedCorrectionData A.meanData A.data ⋯ A.historyTime ⋯ ⋯ A.history A.geometry.δ ⋯
A.terminal ⋯ A.alpha ⋯ (EulerPacketSourceFrequency.truncation k) hn k hk))
:
EulerPhysicalL2Scaling.scale A.parent.ell
(EulerPacketTerminalDatum.initializedExactPhysicalVelocity A.meanData A.data ⋯ A.historyTime ⋯ ⋯ A.history
A.geometry.δ ⋯ A.terminal ⋯ A.alpha ⋯ (EulerPacketSourceFrequency.truncation k) hn k hk Q ⟨0, ⋯⟩ id) = A.high k + A.mean k