Uniform-time reconstruction preserves fixed Sobolev word blocks

Time reconstruction is a fixed bounded linear map. Therefore it commutes with every external and base spatial word and costs no derivative shift.

Direct two-input linear bounds for genuine fixed Sobolev word blocks.

theorem EulerParameterWordGevrey.wordDerivative_pair {P : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (directions : ι → P) (f : P → E) (g : P → F) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) {n : ℕ} (w : Fin n → ι) (x : P) : wordDerivative directions (fun (y : P) => (f y, g y)) w x = (wordDerivative directions f w x, wordDerivative directions g w x)

theorem EulerParameterWordGevrey.wordDerivative_linear_pair {P : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {ι : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (directions : ι → P) (L : E × F →L[ℝ] G) (f : P → E) (g : P → F) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) {n : ℕ} (w : Fin n → ι) (x : P) : wordDerivative directions (fun (y : P) => L (f y, g y)) w x = L (wordDerivative directions f w x, wordDerivative directions g w x)

theorem EulerParameterWordGevrey.wordSum_linear_pair_le {P : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {ι : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [Fintype ι] (directions : ι → P) (L : E × F →L[ℝ] G) (a b : ℝ) (hL : ∀ (p : E) (q : F), ‖L (p, q)‖ ≤ a * ‖p‖ + b * ‖q‖) (f : P → E) (g : P → F) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) (x : P) : wordSum directions (fun (y : P) => L (f y, g y)) n x ≤ a * wordSum directions f n x + b * wordSum directions g n x

theorem EulerParameterWordGevrey.baseSize_linear_pair_le {P : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {ι : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [Fintype ι] (directions : ι → P) (q : ℕ) (L : E × F →L[ℝ] G) (a b : ℝ) (hL : ∀ (p : E) (r : F), ‖L (p, r)‖ ≤ a * ‖p‖ + b * ‖r‖) (f : P → E) (g : P → F) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (x : P) : baseSize directions q (fun (y : P) => L (f y, g y)) x ≤ a * baseSize directions q f x + b * baseSize directions q g x

theorem EulerParameterWordGevrey.block_linear_pair_le {P : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {ι : Type u_5} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] [Fintype ι] (directions : ι → P) (q : ℕ) (L : E × F →L[ℝ] G) (a b : ℝ) (hL : ∀ (p : E) (r : F), ‖L (p, r)‖ ≤ a * ‖p‖ + b * ‖r‖) (f : P → E) (g : P → F) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (n : ℕ) (x : P) : block directions q (fun (y : P) => L (f y, g y)) n x ≤ a * block directions q f n x + b * block directions q g n x

@[instance_reducible]

noncomputable def EulerTimeH1SobolevReconstruction.instTimeH1SobolevReconstruction1 {E : Type u_2} [NormedAddCommGroup E] (T : ℝ) : NormedAddCommGroup ↥(EulerTimeLp.TimeLp T E)

Cache the standard NormedAddCommGroup (TimeLp T E) instance to shorten typeclass synthesis.

Equations

• EulerTimeH1SobolevReconstruction.instTimeH1SobolevReconstruction1 T = inferInstance

@[instance_reducible]

noncomputable def EulerTimeH1SobolevReconstruction.instTimeH1SobolevReconstruction2 {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) : NormedSpace ℝ ↥(EulerTimeLp.TimeLp T E)

Cache the standard NormedSpace ℝ (TimeLp T E) instance to shorten typeclass synthesis.

Equations

• EulerTimeH1SobolevReconstruction.instTimeH1SobolevReconstruction2 T = inferInstance

@[instance_reducible]

noncomputable def EulerTimeH1SobolevReconstruction.instTimeH1SobolevReconstruction3 {E : Type u_2} [NormedAddCommGroup E] (T : ℝ) : NormedAddCommGroup C(↑(Set.Icc 0 T), E)

Cache the standard NormedAddCommGroup C(Icc (0 : ℝ) T,E) instance to shorten typeclass synthesis.

Equations

• EulerTimeH1SobolevReconstruction.instTimeH1SobolevReconstruction3 T = inferInstance

@[instance_reducible]

noncomputable def EulerTimeH1SobolevReconstruction.instTimeH1SobolevReconstruction4 {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (T : ℝ) : NormedSpace ℝ C(↑(Set.Icc 0 T), E)

Cache the standard NormedSpace ℝ C(Icc (0 : ℝ) T,E) instance to shorten typeclass synthesis.

Equations

• EulerTimeH1SobolevReconstruction.instTimeH1SobolevReconstruction4 T = inferInstance

theorem EulerTimeH1SobolevReconstruction.reconstruction_block_le {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype ι] (directions : ι → P) (q : ℕ) (T : ℝ) (hT : 0 < T) (p v : P → ↥(EulerTimeLp.TimeLp T E)) (hp : ContDiff ℝ (↑⊤) p) (hv : ContDiff ℝ (↑⊤) v) (n : ℕ) (x : P) : EulerParameterWordGevrey.block directions q (fun (y : P) => (EulerTimeH1Reconstruction.reconstruction T ⋯) (p y, v y)) n x ≤ T⁻¹ * √T * EulerParameterWordGevrey.block directions q p n x + 2 * √T * EulerParameterWordGevrey.block directions q v n x

The exact finite Sobolev block is bounded by the blocks of the L² value and its genuine L² time derivative.

theorem EulerTimeH1SobolevReconstruction.reconstruction_block_gevrey {P : Type u_1} {E : Type u_2} {ι : Type u_3} [NormedAddCommGroup P] [NormedSpace ℝ P] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fintype ι] (directions : ι → P) (q : ℕ) (T : ℝ) (hT : 0 < T) (p v : P → ↥(EulerTimeLp.TimeLp T E)) (hp : ContDiff ℝ (↑⊤) p) (hv : ContDiff ℝ (↑⊤) v) (R C D : ℝ) (d : ℕ) (hbp : ∀ (n : ℕ) (x : P), EulerParameterWordGevrey.block directions q p n x ≤ C * EulerGevrey.majorant R d n) (hbv : ∀ (n : ℕ) (x : P), EulerParameterWordGevrey.block directions q v n x ≤ D * EulerGevrey.majorant R d n) (n : ℕ) (x : P) : EulerParameterWordGevrey.block directions q (fun (y : P) => (EulerTimeH1Reconstruction.reconstruction T ⋯) (p y, v y)) n x ≤ (T⁻¹ * √T * C + 2 * √T * D) * EulerGevrey.majorant R d n

Uniform time evaluation spends neither a spatial derivative nor an external factorial shift and preserves the original radius.