A fixed source budget for the joined transverse inverse #
Every hypothesis is a coefficient, time-length, or homogeneous-propagator bound. The radius guards use unit forcing amplitude and do not depend on the forcing, its amplitude, its derivative shift, or the recursive grade. Coercivity is required only on the actual history interval [0,τ].
@[instance_reducible]
noncomputable def
EulerTransversePacketJoin.instTransversePacketBudget1
{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
EulerTransversePacketJoin.instTransversePacketBudget2
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
:
Cache the standard NormedRing (Space →ᵇ U →L[ℝ] U) instance to shorten typeclass
synthesis.
Instances For
structure
EulerTransversePacketJoin.Budget
{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τ ⋯))
(ι : Type u_2)
[Fintype ι]
(q : ℕ)
:
Source-only quantitative data, fixed once for all forcing profiles and grades.
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ℝ. - CH : ℝ
CH 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
- history_weak : 2 * EulerTransverseFixedSobolev.blockCost ι q τ self.Rc self.C₀ self.C₁ self.CH (D.initial τ hτ ⋯).frameLower 1 * (EulerParameterWordGevrey.sobolevCoefficientRadius ι self.Rc + 1) ≤ self.R
- history_strong : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q (D.initial τ hτ ⋯).frameLower self.Rc self.C₀ (EulerParameterWordGevrey.accelerationBlockAmplitude ι q self.Rc self.C₀ self.C₁ 1 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι self.Rc + 1) ≤ self.R
- history_uniform : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q (D.initial τ hτ ⋯).frameLower self.Rc self.C₀ (EulerParameterWordGevrey.accelerationBlockAmplitude ι q self.Rc self.C₀ self.C₁ 1 (EulerFixedEvolutionSobolev.traceCost τ)) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι self.Rc + 1) ≤ self.R
- forward_inverse : 2 * EulerTimeLpGramGevrey.gramCost (D.tail τ ⋯ hτT).frameLower self.C₀ 1 * (self.Rc + 1) ≤ self.Ri
- forward_radius : 2 * EulerLinearDuhamel.forwardSobolevCost ι q (D.T - τ) self.C (EulerFixedEvolutionSobolev.traceCost τ) (EulerSourceCylinderForwardSobolev.forcingCost ι q self.Ri self.C₀ * 1) (18 * self.Ri * self.C₀ * self.C₁) (4 * self.Ri) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι (4 * self.Ri) + 1) ≤ self.R
- propagator (t s : ↑(Set.Icc 0 (D.T - τ))) : s ≤ t → ∀ (x : EulerSmoothLimit.Space), ‖x‖ ≤ 1 / 2 → ‖((EulerLinearFundamentalExistence.fundamentalPath (D.T - τ) ⋯ (EulerSourceForwardCoefficient.sourceGenerator (D.tail τ ⋯ hτT).frame (D.tail τ ⋯ hτT).frameDerivative (D.tail τ ⋯ hτT).frameLower ⋯ ⋯)).forward t) x ∘SL ((EulerLinearFundamentalExistence.fundamentalPath (D.T - τ) ⋯ (EulerSourceForwardCoefficient.sourceGenerator (D.tail τ ⋯ hτT).frame (D.tail τ ⋯ hτT).frameDerivative (D.tail τ ⋯ hτT).frameLower ⋯ ⋯)).backward s) x‖ ≤ self.C * self.g t / self.g s
Instances For
noncomputable def
EulerTransversePacketJoin.Budget.fullProfile
{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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D τ hτ hτT B ι q)
:
Full profile, given by EulerElapsedTimePathGluing.profile D.T τ hτ.le hτT.le L.g L.initial_one.
Equations
- L.fullProfile = EulerElapsedTimePathGluing.profile D.T τ ⋯ ⋯ L.g ⋯
Instances For
theorem
EulerTransversePacketJoin.Budget.fullProfile_pos
{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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D τ hτ hτT B ι q)
(t : ↑(Set.Icc 0 D.T))
:
theorem
EulerTransversePacketJoin.Budget.radius_bounds
{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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D τ hτ hτT B ι q)
:
noncomputable def
EulerTransversePacketJoin.Budget.velocityCost
{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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D τ hτ hτT B ι q)
:
Velocity cost, given by 3*sobolevCoefficientAmplitude ι q L.Rc L.C₀*traceCost τ + 3*sobolevCoefficientAmplitude ι q L.Rc L.C₀.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerTransversePacketJoin.Budget.derivativeCost
{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τ ⋯)}
{ι : Type u_2}
[Fintype ι]
{q : ℕ}
(L : Budget D τ hτ hτT B ι q)
:
Derivative cost as an element of ℝ.
Equations
- One or more equations did not get rendered due to their size.