Every available finite derivative word of the actual viscous mild solution satisfies its differentiated L² equation.

def EulerMildWordEquation.mapPath (period : ℝ) [Fact (0 < period)] {p q : ℕ} (T : ℝ) (A : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period p)) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period p))

Applying a bounded linear spatial map to an actual continuous Sobolev time path.

Equations

• EulerMildWordEquation.mapPath period T A u = { toFun := fun (t : ↑(Set.Icc 0 T)) => A (u t), continuous_toFun := ⋯ }

theorem EulerMildWordEquation.map_duhamel (period : ℝ) [Fact (0 < period)] {p q : ℕ} (A : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period p)) (hA : ∀ (v : NNReal) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)), A ((EulerSobolevHeat.heatOperator period q v) u) = (EulerSobolevHeat.heatOperator period p v) (A u)) (ν T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (t : ℝ) : A (EulerDuhamelDifferentiation.duhamel period ν T hT f t) = EulerDuhamelDifferentiation.duhamel period ν T hT (mapPath period T A f) t

Every bounded heat-commuting spatial map commutes with the actual Duhamel integral.

theorem EulerMildWordEquation.viscous_mild_truncated_formula (period : ℝ) [Fact (0 < period)] {q : ℕ} (ν : ℝ) (hν : 0 < ν) (T : ℝ) (hT : 0 ≤ T) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (F : ↑(Set.Icc 0 T) → ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) → ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hF : Continuous fun (p : ↑(Set.Icc 0 T) × ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) => F p.1 p.2) (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) (F (Set.projIcc 0 T hT (↑t - r)) (u (Set.projIcc 0 T hT (↑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 (EulerVolterraConvolution.pathNonlinearity T F hF u) ↑t

The gained-kernel mild formula implies the ordinary Duhamel formula at the lower Sobolev order.

theorem EulerMildWordEquation.viscous_mild_block_hasDerivAt (period : ℝ) [Fact (0 < period)] {p q : ℕ} (hp : 2 ≤ p) (A : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period p)) (hA : ∀ (v : NNReal) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)), A ((EulerSobolevHeat.heatOperator period q v) u) = (EulerSobolevHeat.heatOperator period p v) (A u)) (ν : ℝ) (hν : 0 < ν) (T : ℝ) (hT : 0 ≤ T) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (F : ↑(Set.Icc 0 T) → ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) → ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hF : Continuous fun (p : ↑(Set.Icc 0 T) × ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) => F p.1 p.2) (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) (F (Set.projIcc 0 T hT (↑t - r)) (u (Set.projIcc 0 T hT (↑t - r))))) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (A ((EulerCylinderSobolevSpace.truncateOperator period q) (EulerVolterraConvolution.extendPath T hT u r)))) (ν • (EulerSobolevHeatGenerator.laplacianEvaluation period p hp) (A ((EulerCylinderSobolevSpace.truncateOperator period q) (u ⟨t, ⋯⟩))) + EulerCylinderSobolevSpace.value period (A (F ⟨t, ⋯⟩ (u ⟨t, ⋯⟩)))) t

Any bounded heat-commuting derivative block of the constructed mild solution satisfies its actual L² evolution.

noncomputable def EulerMildWordEquation.availableWordBlock (period : ℝ) [Fact (0 < period)] {q n : ℕ} (h : n + 2 ≤ q) (w : Fin n → Fin 4) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q) →L[ℝ] ↥(EulerCylinderSobolevSpace.SobolevSpace period 2)

The actual derivative block of a field with enough total Sobolev regularity.

Equations

• EulerMildWordEquation.availableWordBlock period h w = EulerSobolevWordBlocks.wordBlock period 2 n w ∘SL EulerCylinderSobolevSpace.restrictOperator period ⋯

theorem EulerMildWordEquation.availableWordBlock_value (period : ℝ) [Fact (0 < period)] {q n : ℕ} (h : n + 2 ≤ q) (w : Fin n → Fin 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : EulerCylinderSobolevSpace.value period ((availableWordBlock period h w) u) = EulerCylinderSobolevSpace.word period u ⋯ w

This available block is exactly the chosen derivative word as an L² field.

theorem EulerMildWordEquation.availableWordBlock_heat (period : ℝ) [Fact (0 < period)] {q n : ℕ} (h : n + 2 ≤ q) (w : Fin n → Fin 4) (v : NNReal) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (availableWordBlock period h w) ((EulerSobolevHeat.heatOperator period q v) u) = (EulerSobolevHeat.heatOperator period 2 v) ((availableWordBlock period h w) u)

Actual derivative-word blocks commute with heat, including the endpoint at zero variance.

theorem EulerMildWordEquation.word_truncate_coordinate (period : ℝ) [Fact (0 < period)] {q n : ℕ} (hn : n ≤ q) (w : Fin n → Fin 4) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) : EulerCylinderSobolevSpace.word period ((EulerCylinderSobolevSpace.truncateOperator period q) u) hn w = EulerCylinderSobolevSpace.word period u ⋯ w

Truncation preserves every derivative coordinate still within its range.

theorem EulerMildWordEquation.viscous_mild_word_hasDerivAt (period : ℝ) [Fact (0 < period)] {q n : ℕ} (h : n + 2 ≤ q) (w : Fin n → Fin 4) (ν : ℝ) (hν : 0 < ν) (T : ℝ) (hT : 0 ≤ T) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (F : ↑(Set.Icc 0 T) → ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) → ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (hF : Continuous fun (p : ↑(Set.Icc 0 T) × ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) => F p.1 p.2) (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) (F (Set.projIcc 0 T hT (↑t - r)) (u (Set.projIcc 0 T hT (↑t - r))))) (t : ℝ) (ht : t ∈ Set.Ioo 0 T) : HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.word period (EulerVolterraConvolution.extendPath T hT u r) ⋯ w) (ν • (EulerSobolevHeatGenerator.laplacianEvaluation period 2 viscous_mild_word_hasDerivAt._proof_3) ((availableWordBlock period h w) ((EulerCylinderSobolevSpace.truncateOperator period q) (u ⟨t, ⋯⟩))) + EulerCylinderSobolevSpace.word period (F ⟨t, ⋯⟩ (u ⟨t, ⋯⟩)) ⋯ w) t

Every finite derivative word below the source's Sobolev margin obeys the differentiated L² equation.