Exact compatibility of the actual heat regularizations with highest derivative blocks.
theorem
EulerRegularizedTopBlocks.heatRegularizer_word
(period : ℝ)
[Fact (0 < period)]
{q m : ℕ}
(n : ℕ)
(hm : m ≤ q)
(w : Fin m → Fin 4)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
:
EulerCylinderSobolevSpace.word period ((EulerHeatRegularizedPaths.heatRegularizer period q n) u) ⋯ w = (EulerGaussianCylinderHeat.cylinderHeat period (EulerHeatRegularizedPaths.regularizerVariance n))
(EulerCylinderSobolevSpace.word period u hm w)
Every preexisting derivative word of a genuine heat regularizer is regularized by the same L² heat operator.
noncomputable def
EulerRegularizedTopBlocks.maximalApproximation
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
(T : ℝ)
(n : ℕ)
(u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
:
The actual regularized state, retained at the full maximal-regularity spatial order.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerRegularizedTopBlocks.maximalApproximation_low
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
(T : ℝ)
(n : ℕ)
(u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
:
(ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.restrictOperator period ⋯))
(maximalApproximation period q T n u) = EulerHeatRegularizedPaths.pathHeat period (q + 1) T (EulerHeatRegularizedPaths.regularizerVariance n) u
Restricting the maximal-regularity approximation is the genuine original-order heat path.
theorem
EulerRegularizedTopBlocks.maximalApproximation_low_tendsto
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
(T : ℝ)
(u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
:
Filter.Tendsto
(fun (n : ℕ) =>
(ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.restrictOperator period ⋯))
(maximalApproximation period q T n u))
Filter.atTop (nhds u)
The full approximation converges uniformly in the original actual Sobolev topology.
theorem
EulerRegularizedTopBlocks.maximalApproximation_word
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
(T : ℝ)
(n : ℕ)
(u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(w : Fin q → Fin 4)
:
(ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerSobolevWordBlocks.wordBlock period 2 q w))
(maximalApproximation period q T n u) = (ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) (EulerCylinderSobolevSpace.truncateOperator period 2))
(EulerRegularizedMildEquation.regularizedState period T n
(EulerMildWordEquation.mapPath period T (EulerMildTopWord.boundedWordBlock period 1 q ⋯ w) u))
Every top derivative block of the full approximation is exactly the corresponding H² approximation of the actual H¹ word solution.