Actual highest derivative words preserve the gained-derivative heat mild formula.
theorem
EulerMildTopWord.truncate_mild_integral
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(ν : ℝ)
(hν : 0 < ν)
(T : ℝ)
(hT : 0 ≤ T)
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(t : ↑(Set.Icc 0 T))
:
(EulerCylinderSobolevSpace.truncateOperator period q)
(∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r) (EulerVolterraConvolution.extendPath T hT f (↑t - r))) = EulerDuhamelDifferentiation.duhamel period ν T hT f ↑t
The gained-kernel integral has exactly the ordinary Duhamel value after actual truncation.
theorem
EulerMildTopWord.mild_of_truncated_formula
(period : ℝ)
[Fact (0 < period)]
(ν : ℝ)
(hν : 0 < ν)
(T : ℝ)
(hT : 0 ≤ T)
(u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period 1))
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 0)))
(u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period 1)))
(hsol :
∀ (t : ↑(Set.Icc 0 T)),
(EulerCylinderSobolevSpace.truncateOperator period 0) (u t) = (EulerSobolevHeatGenerator.heatFlow period 0 ν ↑t) ((EulerCylinderSobolevSpace.truncateOperator period 0) u₀) + EulerDuhamelDifferentiation.duhamel period ν T hT f ↑t)
(t : ↑(Set.Icc 0 T))
:
u t = (EulerSobolevHeat.heatOperator period 1 (2 * ν * ↑t).toNNReal) u₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period 0 ν hν r) (EulerVolterraConvolution.extendPath T hT f (↑t - r))
An actual continuous H¹ path is the gained-kernel mild solution as soon as its genuine L² truncation obeys Duhamel.
noncomputable def
EulerMildTopWord.boundedWordBlock
(period : ℝ)
[Fact (0 < period)]
(p n : ℕ)
{q : ℕ}
(h : p + n ≤ q)
(w : Fin n → Fin 4)
:
↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period p)
A genuine bounded derivative block with an arbitrary available Sobolev margin.
Equations
- EulerMildTopWord.boundedWordBlock period p n h w = EulerSobolevWordBlocks.wordBlock period p n w ∘SL EulerCylinderSobolevSpace.restrictOperator period h
Instances For
theorem
EulerMildTopWord.boundedWordBlock_value
(period : ℝ)
[Fact (0 < period)]
(p n : ℕ)
{q : ℕ}
(h : p + n ≤ q)
(w : Fin n → Fin 4)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
:
EulerCylinderSobolevSpace.value period ((boundedWordBlock period p n h w) u) = EulerCylinderSobolevSpace.word period u ⋯ w
A bounded block has the exact underlying derivative word.
theorem
EulerMildTopWord.boundedWordBlock_heat
(period : ℝ)
[Fact (0 < period)]
(p n : ℕ)
{q : ℕ}
(h : p + n ≤ q)
(w : Fin n → Fin 4)
(v : NNReal)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
:
(boundedWordBlock period p n h w) ((EulerSobolevHeat.heatOperator period q v) u) = (EulerSobolevHeat.heatOperator period p v) ((boundedWordBlock period p n h w) u)
Every bounded actual word block commutes with the genuine heat semigroup.
theorem
EulerMildTopWord.boundedWordBlock_truncate
(period : ℝ)
[Fact (0 < period)]
(q : ℕ)
(w : Fin q → Fin 4)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
:
(EulerCylinderSobolevSpace.truncateOperator period 0) ((boundedWordBlock period 1 q ⋯ w) u) = (boundedWordBlock period 0 q ⋯ w) ((EulerCylinderSobolevSpace.truncateOperator period q) u)
Forgetting the last output derivative of a word block agrees with restricting the input.
theorem
EulerMildTopWord.truncated_formula
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(ν : ℝ)
(hν : 0 < ν)
(T : ℝ)
(hT : 0 ≤ T)
(u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(hsol :
∀ (t : ↑(Set.Icc 0 T)),
u t = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) u₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r) (EulerVolterraConvolution.extendPath T hT f (↑t - r)))
(t : ↑(Set.Icc 0 T))
:
(EulerCylinderSobolevSpace.truncateOperator period q) (u t) = (EulerSobolevHeatGenerator.heatFlow period q ν ↑t) ((EulerCylinderSobolevSpace.truncateOperator period q) u₀) + EulerDuhamelDifferentiation.duhamel period ν T hT f ↑t
The actual gained-derivative formula implies its ordinary lower-order form for a continuous source.
theorem
EulerMildTopWord.top_word_truncated
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(ν T : ℝ)
(hT : 0 ≤ T)
(u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(hsol :
∀ (t : ↑(Set.Icc 0 T)),
(EulerCylinderSobolevSpace.truncateOperator period q) (u t) = (EulerSobolevHeatGenerator.heatFlow period q ν ↑t) ((EulerCylinderSobolevSpace.truncateOperator period q) u₀) + EulerDuhamelDifferentiation.duhamel period ν T hT f ↑t)
(w : Fin q → Fin 4)
(t : ↑(Set.Icc 0 T))
:
(EulerCylinderSobolevSpace.truncateOperator period 0) ((boundedWordBlock period 1 q ⋯ w) (u t)) = (EulerSobolevHeatGenerator.heatFlow period 0 ν ↑t)
((EulerCylinderSobolevSpace.truncateOperator period 0) ((boundedWordBlock period 1 q ⋯ w) u₀)) + EulerDuhamelDifferentiation.duhamel period ν T hT
(EulerMildWordEquation.mapPath period T (boundedWordBlock period 0 q ⋯ w) f) ↑t
Actual highest derivative blocks satisfy the lower-order Duhamel identity.
theorem
EulerMildTopWord.top_word_mild
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(ν : ℝ)
(hν : 0 < ν)
(T : ℝ)
(hT : 0 ≤ T)
(u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))))
(hsol :
∀ (t : ↑(Set.Icc 0 T)),
u t = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) u₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r) (EulerVolterraConvolution.extendPath T hT f (↑t - r)))
(w : Fin q → Fin 4)
(t : ↑(Set.Icc 0 T))
:
(boundedWordBlock period 1 q ⋯ w) (u t) = (EulerSobolevHeat.heatOperator period 1 (2 * ν * ↑t).toNNReal) ((boundedWordBlock period 1 q ⋯ w) u₀) + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period 0 ν hν r)
(EulerVolterraConvolution.extendPath T hT
(EulerMildWordEquation.mapPath period T (boundedWordBlock period 0 q ⋯ w) f) (↑t - r))
Every highest-order derivative word of an actual H^(q+1) mild solution is itself an actual H¹ mild solution with its differentiated L² source.