Source-only budgets for the genuine forward transverse problem starting at time zero. The same fixed radius controls unit forcing and unit initial coordinates; there is no history interval or terminal variational problem.
@[instance_reducible]
noncomputable def
EulerTransversePacketForward.instTransversePacketForwardBudget1
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
:
NormedRing (U →L[ℝ] U)
Cache the standard NormedRing (U →L[ℝ] U) instance to shorten typeclass synthesis.
Instances For
@[instance_reducible]
noncomputable def
EulerTransversePacketForward.instTransversePacketForwardBudget2
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
:
Cache the standard NormedRing (Space →ᵇ U →L[ℝ] U) instance to shorten typeclass
synthesis.
Instances For
structure
EulerTransversePacketForward.Budget
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
(D : EulerTransversePacketProvider.Data U)
(ι : Type u_2)
[Fintype ι]
(q : ℕ)
:
Budget data, collecting g, positive, initial_one, neighborhood,
neighborhood_measurable, neighborhood_open and their compatibility conditions.
G of
Budget, of typeC(Icc (0 : ℝ) D.T,ℝ).- neighborhood : Set EulerSmoothLimit.Space
- neighborhood_measurable : MeasurableSet self.neighborhood
- neighborhood_open : IsOpen self.neighborhood
- support_subset : D.support ⊆ self.neighborhood
- neighborhood_halfball (x : EulerSmoothLimit.Space) : x ∈ self.neighborhood → ‖x‖ ≤ 1 / 2
- Rc : ℝ
Rc of
Budget, of typeℝ. - C₀ : ℝ
C₀ of
Budget, of typeℝ. - C₁ : ℝ
First-derivative bound coefficient of
Budget, of typeℝ. - C : ℝ
Bound coefficient of
Budget, of typeℝ. - Ri : ℝ
Ri of
Budget, of typeℝ. - R : ℝ
Radius parameter of
Budget, of typeℝ. - frame_bound (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(D.F.field t)) x‖ ≤ self.C₀ * EulerGevrey.majorant self.Rc 0 n
- frameDerivative_bound (n : ℕ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (⇑(D.F₁.field t)) x‖ ≤ self.C₁ * EulerGevrey.majorant self.Rc 0 n
- forward_inverse : 2 * EulerTimeLpGramGevrey.gramCost D.frameLower self.C₀ 1 * (self.Rc + 1) ≤ self.Ri
- propagator (t s : ↑(Set.Icc 0 D.T)) : s ≤ t → ∀ (x : EulerSmoothLimit.Space), ‖x‖ ≤ 1 / 2 → ‖((EulerLinearFundamentalExistence.fundamentalPath D.T ⋯ (EulerSourceForwardCoefficient.sourceGenerator D.frame D.frameDerivative D.frameLower ⋯ ⋯)).forward t) x ∘SL ((EulerLinearFundamentalExistence.fundamentalPath D.T ⋯ (EulerSourceForwardCoefficient.sourceGenerator D.frame D.frameDerivative D.frameLower ⋯ ⋯)).backward s) x‖ ≤ self.C * self.g t / self.g s
Instances For
def
EulerTransversePacketForward.Budget.velocityCost
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D ι q)
:
Velocity cost, given by 3*sobolevCoefficientAmplitude ι q L.Rc L.C₀.
Equations
Instances For
def
EulerTransversePacketForward.Budget.derivativeCost
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D ι q)
:
Derivative cost, given by physicalCost ι q L.Ri L.C₀ L.C₁ 1 1.
Equations
- L.derivativeCost = EulerSourceCylinderTimeBounds.physicalCost ι q L.Ri L.C₀ L.C₁ 1 1
Instances For
def
EulerTransversePacketForward.Budget.commonCost
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D ι q)
:
Common cost, given by L.velocityCost+L.derivativeCost.
Equations
- L.commonCost = L.velocityCost + L.derivativeCost
Instances For
def
EulerTransversePacketForward.Budget.enlargeRadius
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D ι q)
(R' : ℝ)
(hR : L.R ≤ R')
:
Budget D ι q
Enlarge radius as an element of Budget D ι q.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerTransversePacketForward.Budget.velocityCost_nonneg
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D ι q)
:
theorem
EulerTransversePacketForward.Budget.derivativeCost_nonneg
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D ι q)
:
theorem
EulerTransversePacketForward.Budget.commonCost_nonneg
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D ι q)
:
theorem
EulerTransversePacketForward.Budget.velocityCost_le_common
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D ι q)
:
theorem
EulerTransversePacketForward.Budget.derivativeCost_le_common
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D ι q)
:
theorem
EulerTransversePacketForward.Budget.velocity_unit_bound
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D ι q)
{P : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(I : EulerTransversePacketProvider.InitialData P D)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.g ⋯) ((EulerLpCylinderPaths.includePath P D.support ⋯) G.path)))
n 0 ≤ EulerGevrey.majorant L.R d n)
(hinitial :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.g ⋯) (G.fullVelocityPath I)))
n 0 ≤ L.velocityCost * EulerGevrey.majorant L.R (d + 1) n
theorem
EulerTransversePacketForward.Budget.derivative_unit_bound
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D ι q)
{P : ℝ}
[Fact (0 < P)]
{raw : EulerPacketProfileRecursion.VectorField}
(G : EulerTransversePacketProvider.Forcing P D raw)
(I : EulerTransversePacketProvider.InitialData P D)
(directions : ι → EulerLiftedGradientSpace.LiftTangent)
(hdir : ∀ (i : ι), ‖directions i‖ ≤ 1)
(d : ℕ)
(hforce :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.g ⋯) ((EulerLpCylinderPaths.includePath P D.support ⋯) G.path)))
n 0 ≤ EulerGevrey.majorant L.R d n)
(hinitial :
∀ (n : ℕ),
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.translate P a) ↑I.value) n 0 ≤ EulerGevrey.majorant L.R d n)
(n : ℕ)
:
EulerParameterWordGevrey.block directions q
(fun (a : EulerLiftedGradientSpace.LiftTangent) =>
(EulerLpCylinderTranslation.pathTranslate P a)
((EulerContinuousTimeWeight.normalize L.g ⋯) (G.fullDerivativePath I)))
n 0 ≤ L.derivativeCost * EulerGevrey.majorant L.R (d + 1) n