The actual activation geometry supplies H3 in the complete joined packet budget. Source label bounds and the original curvature hypotheses remain inputs; no propagator estimate or chosen growth profile is assumed.
noncomputable def
EulerPacketSourceGeometry.Guards.sourceGrowthProfile
{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)
:
Source growth profile, given by (J.halfBall_controlledGrowth hball).choose.
Equations
- J.sourceGrowthProfile hball = ⋯.choose
Instances For
theorem
EulerPacketSourceGeometry.Guards.sourceGrowthProfile_positive
{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)
(t : ↑(Set.Icc 0 (D.T - τ)))
:
theorem
EulerPacketSourceGeometry.Guards.sourceGrowthProfile_initial
{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)
:
theorem
EulerPacketSourceGeometry.Guards.sourceGrowthProfile_propagator
{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)
:
EulerPacketSourcePropagator.PhysicalGrowth (D.tail τ ⋯ hτT) EulerPacketParentPhysicalBudgets.halfBall
(⇑(J.sourceGrowthProfile hball)) (560 * P.horizon ^ 10 / P.epsilon)
theorem
EulerPacketSourceGeometry.Guards.sourceGrowthProfile_amplitude
{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)
(t : ↑(Set.Icc 0 (D.T - τ)))
:
theorem
EulerPacketSourceGeometry.Guards.primaryAmplitude_bound
{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)
:
noncomputable def
EulerPacketSourceGeometry.Guards.joinedBudget
{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)
(q : ℕ)
(A V : ↑(Set.Icc 0 D.T) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space)
(W : ↑(Set.Icc 0 τ) → EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space)
(F₂ :
EulerMeanCoefficients.SmoothCoefficientPath (↑(Set.Icc 0 τ)) (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))
(ℓ K Ti : ℝ)
(hℓ : 0 ≤ ℓ)
(hℓ1 : ℓ ≤ 1)
(hK : 0 ≤ K)
(hτ1 : τ ≤ 1)
(hTi : τ⁻¹ ≤ Ti)
(hA : ∀ (t : ↑(Set.Icc 0 D.T)), EulerPacketParentLabelBounds.HasLabelBound K (A t))
(hV : ∀ (t : ↑(Set.Icc 0 D.T)), EulerPacketParentLabelBounds.HasLabelBound K (V t))
(hW : ∀ (t : ↑(Set.Icc 0 τ)), EulerPacketParentLabelBounds.HasLabelBound K (W t))
(hF :
∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
(D.F.field t) x = ContinuousLinearMap.id ℝ EulerSmoothLimit.Space + fderiv ℝ (A t).field (ℓ • x))
(hF₁ : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), (D.F₁.field t) x = fderiv ℝ (V t).field (ℓ • x))
(hF₂ : ∀ (t : ↑(Set.Icc 0 τ)) (x : EulerSmoothLimit.Space), (F₂.field t) x = fderiv ℝ (W t).field (ℓ • x))
(h₂ :
∀ t ∈ Set.Icc 0 τ,
∀ (x : EulerSmoothLimit.Space),
HasDerivWithinAt (fun (s : ℝ) => (EulerVolterraConvolution.extendPath τ ⋯ (D.initial τ hτ ⋯).F₁.field s) x)
((EulerVolterraConvolution.extendPath τ ⋯ F₂.field t) x) (Set.Icc 0 τ) t)
(hdet :
∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space),
Matrix.det (EulerPacketPiola.operatorMatrix ((D.F.field t) x)) = 1)
(Ω : Set EulerSmoothLimit.Space)
(hΩ : MeasurableSet Ω)
(hΩo : IsOpen Ω)
(hsub : D.support ⊆ Ω)
(hΩball : ∀ x ∈ Ω, ‖x‖ ≤ 1 / 2)
:
EulerTransversePacketJoin.Budget D τ hτ hτT H (Fin 4) q
Joined budget, constructed using EulerPacketParentPhysicalBudgets.joinedBudget.
Equations
- One or more equations did not get rendered due to their size.