Actual primary size and sign estimates on the good, early, and stationary-history portions of the packet horizon. The amplitude is the one selected by its genuine center target size.
Cutoff bound, given by 1+(9/rawBump 0)^3.
Equations
Instances For
Good ratio, given by cutoffBound*(64*Real.exp 6).
Equations
Instances For
theorem
EulerPacketGeometryLowBounds.amplitude_size_of_ratio
{ι : Type u_1}
(G : EulerPacketMovingFrame.PhysicalGeometryData ι)
(value R : ℝ)
(h : value / G.targetSize ≤ R)
:
theorem
EulerPacketGeometryLowBounds.amplitude_nonneg
{ι : Type u_1}
(G : EulerPacketMovingFrame.PhysicalGeometryData ι)
:
noncomputable def
EulerPacketSourceGeometry.Guards.lowGeometry
{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τ ⋯)}
(A : Guards hτ hτT P H)
(hball : 1 / 2 ≤ A.radius)
:
Low geometry, given by A.geometryData {x | ‖x‖ ≤ (1/2 : ℝ)} (by norm_num) (fun _ hx => hx.trans hball).
Equations
- A.lowGeometry hball = A.geometryData {x : EulerSmoothLimit.Space | ‖x‖ ≤ 1 / 2} EulerPacketSourceGeometry.Guards.lowGeometry._proof_1 ⋯
Instances For
noncomputable def
EulerPacketSourceGeometry.Guards.primaryAmplitude
{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τ ⋯)}
(A : Guards hτ hτT P H)
(hball : 1 / 2 ≤ A.radius)
:
Primary amplitude, given by (A.lowGeometry hball).amplitude.
Equations
- A.primaryAmplitude hball = (A.lowGeometry hball).amplitude
Instances For
theorem
EulerPacketSourceGeometry.Guards.primaryAmplitude_nonneg
{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τ ⋯)}
(A : Guards hτ hτT P H)
(hball : 1 / 2 ≤ A.radius)
:
noncomputable def
EulerPacketSourceGeometry.Guards.earlyRatio
{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τ ⋯)}
(_A : Guards hτ hτT P H)
:
Early ratio, given by cutoffBound*(8232*Real.exp 9*P.horizon^5*Real.exp (-(1/(4*P.sigma)))).
Equations
Instances For
theorem
EulerPacketSourceGeometry.Guards.earlyRatio_nonneg
{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τ ⋯)}
(A : Guards hτ hτT P H)
:
theorem
EulerPacketSourceGeometry.Guards.scaledTime_upper
{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τ ⋯)}
(A : Guards hτ hτT P H)
(t : ↑(Set.Icc 0 D.T))
:
theorem
EulerPacketSourceGeometry.Guards.lowGeometry_size
{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τ ⋯)}
(A : Guards hτ hτT P H)
(hball : 1 / 2 ≤ A.radius)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(hx : ‖x‖ ≤ 1 / 2)
:
theorem
EulerPacketSourceGeometry.Guards.cutoff_amplitude_size
{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τ ⋯)}
(A : Guards hτ hτT P H)
(hball : 1 / 2 ≤ A.radius)
(t : ↑(Set.Icc 0 D.T))
(x : EulerSmoothLimit.Space)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
:
A.primaryAmplitude hball * (‖(D.normal.field t) x‖ * ‖EulerPacketPrimaryFactorization.canonicalVelocity τ hτ hτT H (terminal hτ hτT P H A) hs (↑t) x‖) = EulerSpatialCutoffs.innerCutoff x * (A.primaryAmplitude hball * (‖(D.normal.field t) x‖ * ‖EulerPacketPrimaryFactorization.uncutVelocity τ hτ hτT H (terminal hτ hτT P H A) (↑t) x‖))
theorem
EulerPacketSourceGeometry.Guards.good_primary_size
{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τ ⋯)}
(A : Guards hτ hτT P H)
(hball : 1 / 2 ≤ A.radius)
(t : ↑(Set.Icc 0 D.T))
(ht : 1 ≤ EulerPacketMovingFrame.scaledTime τ P.a P.epsilon ↑t)
(x : EulerSmoothLimit.Space)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
:
theorem
EulerPacketSourceGeometry.Guards.good_primary_flux
{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τ ⋯)}
(A : Guards hτ hτT P H)
(hball : 1 / 2 ≤ A.radius)
(t : ↑(Set.Icc 0 D.T))
(ht : 1 ≤ EulerPacketMovingFrame.scaledTime τ P.a P.epsilon ↑t)
(x : EulerSmoothLimit.Space)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
:
theorem
EulerPacketSourceGeometry.Guards.early_primary_size
{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τ ⋯)}
(A : Guards hτ hτT P H)
(hball : 1 / 2 ≤ A.radius)
(t : ↑(Set.Icc 0 D.T))
(ht : EulerPacketMovingFrame.scaledTime τ P.a P.epsilon ↑t ∈ Set.Icc 0 1)
(x : EulerSmoothLimit.Space)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
:
noncomputable def
EulerPacketSourceGeometry.Guards.historySizeCost
{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τ ⋯)}
(A : Guards hτ hτT P H)
:
This cost is computed from the actual stationary endpoint operator. It is used only on the history interval; the good interval keeps its sharp universal target-size ratio.
Equations
Instances For
theorem
EulerPacketSourceGeometry.Guards.historySizeCost_nonneg
{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τ ⋯)}
(A : Guards hτ hτT P H)
:
noncomputable def
EulerPacketSourceGeometry.Guards.historyRatio
{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τ ⋯)}
(A : Guards hτ hτT P H)
:
History ratio, given by cutoffBound*(4*P.horizon*A.historySizeCost/(P.rayScale hτ hτT)) * Real.exp (-(1/(4*P.sigma))).
Equations
Instances For
theorem
EulerPacketSourceGeometry.Guards.historyRatio_nonneg
{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τ ⋯)}
(A : Guards hτ hτT P H)
:
noncomputable def
EulerPacketSourceGeometry.Guards.badRatio
{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τ ⋯)}
(A : Guards hτ hτT P H)
:
Bad ratio, given by A.earlyRatio+A.historyRatio.
Equations
- A.badRatio = A.earlyRatio + A.historyRatio
Instances For
theorem
EulerPacketSourceGeometry.Guards.badRatio_nonneg
{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τ ⋯)}
(A : Guards hτ hτT P H)
:
theorem
EulerPacketSourceGeometry.Guards.badRatio_formula
{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τ ⋯)}
(A : Guards hτ hτT P H)
:
theorem
EulerPacketSourceGeometry.Guards.history_uncut_size
{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τ ⋯)}
(A : Guards hτ hτT P H)
(t : ↑(Set.Icc 0 D.T))
(ht : ↑t ≤ τ)
(x : EulerSmoothLimit.Space)
:
theorem
EulerPacketSourceGeometry.Guards.history_primary_size
{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τ ⋯)}
(A : Guards hτ hτT P H)
(hball : 1 / 2 ≤ A.radius)
(t : ↑(Set.Icc 0 D.T))
(ht : ↑t ≤ τ)
(x : EulerSmoothLimit.Space)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
:
theorem
EulerPacketSourceGeometry.Guards.bad_primary_size
{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τ ⋯)}
(A : Guards hτ hτT P H)
(hball : 1 / 2 ≤ A.radius)
(t : ↑(Set.Icc 0 D.T))
(ht : EulerPacketMovingFrame.scaledTime τ P.a P.epsilon ↑t ≤ 1)
(x : EulerSmoothLimit.Space)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
:
One exponential target-ratio bound covers every time before scaled time one, including the stationary history.