Same-radius history acceleration and time trace

The true fixed-Sobolev inverse estimate passes through the actual Gram acceleration and bounded H¹ reconstruction. For continuous forcing the continuous Gram formula gives the time-uniform acceleration as well. All input and output external radii are identical.

noncomputable def EulerFixedEvolutionSobolev.traceCost (T : ℝ) : ℝ

Trace cost, given by T⁻¹*Real.sqrt T+2*Real.sqrt T.

Equations

• EulerFixedEvolutionSobolev.traceCost T = T⁻¹ * √T + 2 * √T

theorem EulerFixedEvolutionSobolev.traceCost_nonneg (T : ℝ) (hT : 0 ≤ T) : 0 ≤ traceCost T

theorem EulerFixedEvolutionSobolev.weak_radius_bounds (ι : Type u_1) [Fintype ι] (q : ℕ) (T Rc C₀ C₁ CH c Cf R : ℝ) (hT : 0 ≤ T) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCH : 0 ≤ CH) (hCf : 0 ≤ Cf) (hR : 2 * EulerTransverseFixedSobolev.blockCost ι q T Rc C₀ C₁ CH c Cf * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) : 1 ≤ R ∧ EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc ≤ R

theorem EulerFixedEvolutionSobolev.accelerationLp_block_gevrey {X : Type u_1} {U : Type u_2} {E : Type u_3} {ι : Type u_4} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] (directions : ι → X) (hdir : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : X → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : X → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : X) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (Q x)) ((Q₁ x) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hPotential : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (hQ : ContDiff ℝ (↑⊤) Q) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (hH : ContDiff ℝ (↑⊤) H) (Rc C₀ C₁ CH Cf R : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCH : 0 ≤ CH) (hCf : 0 ≤ Cf) (hbQ : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (hbH : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n H x‖ ≤ CH * EulerGevrey.majorant Rc 0 n) (hRweak : 2 * EulerTransverseFixedSobolev.blockCost ι q T Rc C₀ C₁ CH c Cf * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hRstrong : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q c Rc C₀ (EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (f : X → ↥(EulerTimeLp.TimeLp T E)) (hf : ContDiff ℝ (↑⊤) f) (d : ℕ) (hfb : ∀ (n : ℕ) (x : X), EulerParameterWordGevrey.block directions q f n x ≤ Cf * EulerGevrey.majorant R d n) (n : ℕ) (x : X) : EulerParameterWordGevrey.block directions q (fun (y : X) => (EulerTransverseFixedEvolution.accelerationLp T hT (Q y) (Q₁ y) (H y) c hc ⋯ ⋯ K hK ⋯ hsmall) (f y)) n x ≤ EulerGevrey.majorant R (d + 2) n

Actual L² acceleration has the second shift, in the same fixed Hq block.

theorem EulerFixedEvolutionSobolev.velocityPath_block_gevrey {X : Type u_1} {U : Type u_2} {E : Type u_3} {ι : Type u_4} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] (directions : ι → X) (hdir : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : X → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : X → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : X) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (Q x)) ((Q₁ x) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hPotential : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (hQ : ContDiff ℝ (↑⊤) Q) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (hH : ContDiff ℝ (↑⊤) H) (Rc C₀ C₁ CH Cf R : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCH : 0 ≤ CH) (hCf : 0 ≤ Cf) (hbQ : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (hbH : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n H x‖ ≤ CH * EulerGevrey.majorant Rc 0 n) (hRweak : 2 * EulerTransverseFixedSobolev.blockCost ι q T Rc C₀ C₁ CH c Cf * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hRstrong : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q c Rc C₀ (EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hTpos : 0 < T) (f : X → ↥(EulerTimeLp.TimeLp T E)) (hf : ContDiff ℝ (↑⊤) f) (d : ℕ) (hfb : ∀ (n : ℕ) (x : X), EulerParameterWordGevrey.block directions q f n x ≤ Cf * EulerGevrey.majorant R d n) (n : ℕ) (x : X) : EulerParameterWordGevrey.block directions q (fun (y : X) => (EulerTransverseFixedEvolution.velocityPath T hT (Q y) (Q₁ y) (H y) c hc ⋯ ⋯ K hK ⋯ hsmall) (f y)) n x ≤ traceCost T * EulerGevrey.majorant R (d + 2) n

The actual H¹ representative has a uniform-time block estimate with the explicit time-trace cost, and no new external-radius factor.

theorem EulerFixedEvolutionSobolev.continuousVelocity_block_gevrey {X : Type u_1} {U : Type u_2} {E : Type u_3} {ι : Type u_4} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] (directions : ι → X) (hdir : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : X → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : X → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : X) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (Q x)) ((Q₁ x) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hPotential : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (hQ : ContDiff ℝ (↑⊤) Q) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (hH : ContDiff ℝ (↑⊤) H) (Rc C₀ C₁ CH Cf R : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCH : 0 ≤ CH) (hCf : 0 ≤ Cf) (hbQ : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (hbH : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n H x‖ ≤ CH * EulerGevrey.majorant Rc 0 n) (hRweak : 2 * EulerTransverseFixedSobolev.blockCost ι q T Rc C₀ C₁ CH c Cf * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hRstrong : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q c Rc C₀ (EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hTpos : 0 < T) (hT1 : T ≤ 1) (f : X → C(↑(Set.Icc 0 T), E)) (hf : ContDiff ℝ (↑⊤) f) (d : ℕ) (hfb : ∀ (n : ℕ) (x : X), EulerParameterWordGevrey.block directions q f n x ≤ Cf * EulerGevrey.majorant R d n) (n : ℕ) (x : X) : EulerParameterWordGevrey.block directions q (fun (y : X) => (EulerTransverseFixedEvolution.velocityPath T hT (Q y) (Q₁ y) (H y) c hc ⋯ ⋯ K hK ⋯ hsmall) (EulerTimeLp.pathLp T hT (f y))) n x ≤ traceCost T * EulerGevrey.majorant R (d + 2) n

A bounded continuous-time forcing family enters the actual time-L² space with no amplitude loss on a source interval of length at most one.

theorem EulerFixedEvolutionSobolev.classicalAcceleration_block_gevrey {X : Type u_1} {U : Type u_2} {E : Type u_3} {ι : Type u_4} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [Fintype ι] (directions : ι → X) (hdir : ∀ (i : ι), ‖directions i‖ ≤ 1) (q : ℕ) (T : ℝ) (hT : 0 ≤ T) (Q Q₁ : X → C(↑(Set.Icc 0 T), U →L[ℝ] E)) (H : X → C(↑(Set.Icc 0 T), E →L[ℝ] E)) (c : ℝ) (hc : 0 < c) (hLower : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2) (hd : ∀ (x : X) (t : ↑(Set.Icc 0 T)), HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT (Q x)) ((Q₁ x) t) (Set.Icc 0 T) ↑t) (K : ℝ) (hK : 0 ≤ K) (hPotential : ∀ (x : X) (t : ↑(Set.Icc 0 T)) (v : E), inner ℝ (((H x) t) v) v ≤ K * ‖v‖ ^ 2) (hsmall : K * (T ^ 2 / 2) ≤ 1 / 2) (hQ : ContDiff ℝ (↑⊤) Q) (hQ₁ : ContDiff ℝ (↑⊤) Q₁) (hH : ContDiff ℝ (↑⊤) H) (Rc C₀ C₁ CH Cf R : ℝ) (hRc : 0 ≤ Rc) (hC₀ : 0 ≤ C₀) (hC₁ : 0 ≤ C₁) (hCH : 0 ≤ CH) (hCf : 0 ≤ Cf) (hbQ : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n Q x‖ ≤ C₀ * EulerGevrey.majorant Rc 0 n) (hbQ₁ : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n Q₁ x‖ ≤ C₁ * EulerGevrey.majorant Rc 0 n) (hbH : ∀ (n : ℕ) (x : X), ‖iteratedFDeriv ℝ n H x‖ ≤ CH * EulerGevrey.majorant Rc 0 n) (hRweak : 2 * EulerTransverseFixedSobolev.blockCost ι q T Rc C₀ C₁ CH c Cf * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hRstrong : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q c Rc C₀ (EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf 1) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (hTpos : 0 < T) (hT1 : T ≤ 1) (hRuniform : 2 * EulerTimeLpGramSobolev.gramBlockCost ι q c Rc C₀ (EulerParameterWordGevrey.accelerationBlockAmplitude ι q Rc C₀ C₁ Cf (traceCost T)) * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R) (f : X → C(↑(Set.Icc 0 T), E)) (hf : ContDiff ℝ (↑⊤) f) (d : ℕ) (hfb : ∀ (n : ℕ) (x : X), EulerParameterWordGevrey.block directions q f n x ≤ Cf * EulerGevrey.majorant R d n) (n : ℕ) (x : X) : EulerParameterWordGevrey.block directions q (fun (y : X) => EulerTransverseFixedEvolution.classicalAcceleration T hT (Q y) (Q₁ y) (H y) c hc ⋯ ⋯ K hK ⋯ hsmall (f y)) n x ≤ EulerGevrey.majorant R (d + 3) n

The genuine continuous Gram acceleration has the third shift; its norm includes the endpoint needed for gluing the first-order evolution.