Genuine coefficient and metric budgets persist under restriction to a partial time interval.
Actual correction coefficient data restricted along continuous time maps.
def
EulerCorrectionOperators.CoefficientPath.comp
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : Type u_1}
{U : Type u_2}
[TopologicalSpace T]
[TopologicalSpace U]
(A : CoefficientPath period q T)
(f : C(U, T))
:
CoefficientPath period q U
Restrict the actual spatial coefficient and its jet along a continuous parameter map.
Equations
- EulerCorrectionOperators.CoefficientPath.comp period A f = { coefficient := fun (t : U) => A.coefficient (f t), jet := fun (t : U) => A.jet (f t), continuous := ⋯ }
Instances For
noncomputable def
EulerCorrectionOperators.CorrectionData.comp
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : Type u_1}
{U : Type u_2}
[TopologicalSpace T]
[TopologicalSpace U]
(D : CorrectionData period q T)
(f : C(U, T))
:
CorrectionData period q U
Restrict every actual coefficient, background field, and residual along the same time map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerCorrectionOperators.CorrectionData.comp_source
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T : Type u_1}
{U : Type u_2}
[TopologicalSpace T]
[TopologicalSpace U]
(D : CorrectionData period q T)
(f : C(U, T))
(hq : 6 ≤ q)
(t : U)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
:
The restricted correction source is the original actual source at the restricted time.
theorem
EulerCorrectionOperators.CorrectionData.comp_quadraticDuhamel
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(hq : 6 ≤ q)
(ν : ℝ)
(hν : 0 < ν)
{T S : ℝ}
(hT : 0 ≤ T)
(hTS : T ≤ S)
(D : CorrectionData period q ↑(Set.Icc 0 S))
(u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
(u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(t : ↑(Set.Icc 0 T))
:
EulerQuadraticSource.quadraticDuhamel period ν hν hT ⋯
(coefficients period (comp period D (EulerQuadraticSource.timeInclusion hTS)) hq) u₀ u t = EulerQuadraticSource.quadraticDuhamel period ν hν hT hTS (coefficients period D hq) u₀ u t
Restricting the concrete data gives precisely the same nonlinear mild equation on a shorter interval.
theorem
EulerCorrectionBudgetRestriction.extend_restriction_eq
{E : Type u_1}
[NormedAddCommGroup E]
{T S : ℝ}
(hT : 0 ≤ T)
(hS : 0 ≤ S)
(hTS : T ≤ S)
(f : C(↑(Set.Icc 0 S), E))
(t : ℝ)
(ht : t ∈ Set.Icc 0 T)
:
EulerVolterraConvolution.extendPath T hT (f.comp (EulerQuadraticSource.timeInclusion hTS)) t = EulerVolterraConvolution.extendPath S hS f t
Clamped restriction agrees with the original continuous path at every time in the shorter interval.
theorem
EulerCorrectionBudgetRestriction.hasDerivAt_restriction
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
{T S : ℝ}
(hT : 0 ≤ T)
(hS : 0 ≤ S)
(hTS : T ≤ S)
(f f' : C(↑(Set.Icc 0 S), E))
(hf :
∀ t ∈ Set.Ioo 0 S,
HasDerivAt (EulerVolterraConvolution.extendPath S hS f) (EulerVolterraConvolution.extendPath S hS f' t) t)
(t : ℝ)
(ht : t ∈ Set.Ioo 0 T)
:
HasDerivAt (EulerVolterraConvolution.extendPath T hT (f.comp (EulerQuadraticSource.timeInclusion hTS)))
(EulerVolterraConvolution.extendPath T hT (f'.comp (EulerQuadraticSource.timeInclusion hTS)) t) t
Restriction of a genuine time derivative gives the same genuine derivative in the shorter interval.
def
EulerCorrectionBudgetRestriction.SpatialBudget.restrict
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T S : ℝ}
{hq : 6 ≤ q + 1}
{D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 S)}
{N : ℕ}
{R : C(↑(Set.Icc 0 S), ℝ)}
(B : EulerCorrectionEnergyData.SpatialBudget period hq D N R)
(hTS : T ≤ S)
:
EulerCorrectionEnergyData.SpatialBudget period hq
(EulerCorrectionOperators.CorrectionData.comp period D (EulerQuadraticSource.timeInclusion hTS)) N
(R.comp (EulerQuadraticSource.timeInclusion hTS))
Every concrete spatial budget restricts with exactly the same numerical constants.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
EulerCorrectionBudgetRestriction.MetricBudget.restrict
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
{T S : ℝ}
{hS : 0 ≤ S}
{D : EulerCorrectionOperators.CorrectionData period (q + 1) ↑(Set.Icc 0 S)}
(K : EulerCorrectionEnergyData.MetricBudget period S hS D)
(hT : 0 ≤ T)
(hTS : T ≤ S)
:
EulerCorrectionEnergyData.MetricBudget period T hT
(EulerCorrectionOperators.CorrectionData.comp period D (EulerQuadraticSource.timeInclusion hTS))
The actual inverse metric and its genuine derivative restrict with unchanged numerical budgets.
Equations
- One or more equations did not get rendered due to their size.