Genuine Sobolev derivative words and time fields are independent of harmless order reindexing.

theorem EulerSobolevWordValueIdentity.word_of_value_eq (period : ℝ) [Fact (0 < period)] {p q n : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period p)) (v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (huv : EulerCylinderSobolevSpace.value period u = EulerCylinderSobolevSpace.value period v) (hp : n ≤ p) (hq : n ≤ q) (w : Fin n → Fin 4) : EulerCylinderSobolevSpace.word period u hp w = EulerCylinderSobolevSpace.word period v hq w

Equal actual L² fields have identical strong derivative words at every shared Sobolev order.

theorem EulerSobolevWordValueIdentity.boundedWordBlock_of_value_eq (period : ℝ) [Fact (0 < period)] {p q r n : ℕ} (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period p)) (v : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (huv : EulerCylinderSobolevSpace.value period u = EulerCylinderSobolevSpace.value period v) (hp : r + n ≤ p) (hq : r + n ≤ q) (w : Fin n → Fin 4) : (EulerMildTopWord.boundedWordBlock period r n hp w) u = (EulerMildTopWord.boundedWordBlock period r n hq w) v

Every actual bounded derivative block depends only on its underlying field when the required derivatives exist.

noncomputable def EulerSobolevWordValueIdentity.reindexMaximalTime (period : ℝ) [Fact (0 < period)] (q : ℕ) (T : ℝ) (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q)))) : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1 + 1)))

The genuine maximal-regularity time field reindexed from H^(2+q) to H^((q+1)+1).

Equations

• EulerSobolevWordValueIdentity.reindexMaximalTime period q T U = (ContinuousLinearMap.compLpL 2 (EulerTimeLp.timeMeasure T) (EulerCylinderSobolevSpace.restrictOperator period ⋯)) U

theorem EulerSobolevWordValueIdentity.reindexMaximalTime_value (period : ℝ) [Fact (0 < period)] (q : ℕ) (T : ℝ) (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q)))) : (fun (t : ℝ) => EulerCylinderSobolevSpace.value period (↑↑(reindexMaximalTime period q T U) t)) =ᵐ[EulerTimeLp.timeMeasure T] fun (t : ℝ) => EulerCylinderSobolevSpace.value period (↑↑U t)

This actual reindexing preserves the represented L² field almost everywhere in time.

theorem EulerSobolevWordValueIdentity.reindexMaximalTime_restriction (period : ℝ) [Fact (0 < period)] {q : ℕ} (T : ℝ) (hT : 0 ≤ T) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (U : ↥(EulerTimeLp.TimeLp T ↥(EulerCylinderSobolevSpace.SobolevSpace period (2 + q)))) (hU : Filter.Tendsto (fun (n : ℕ) => EulerTimeLp.pathLp T hT (EulerRegularizedTopBlocks.maximalApproximation period q T n u)) Filter.atTop (nhds U)) : (fun (t : ℝ) => (EulerCylinderSobolevSpace.truncateOperator period (q + 1)) (↑↑(reindexMaximalTime period q T U) t)) =ᵐ[EulerTimeLp.timeMeasure T] EulerVolterraConvolution.extendPath T hT u

The reindexed genuine maximal-regularity field restricts to the original continuous solution.