The genuine Bochner Gram inverse in fixed Sobolev word blocks #
The coefficient family alone pays a fixed Sobolev cost. The actual right side and solution are measured in the identical ordered-word blocks.
noncomputable def
EulerTimeLpGramSobolev.gramBlockCost
(ι : Type u_1)
[Fintype ι]
(q : ℕ)
(c Rc C D : ℝ)
:
Polynomial cost of the actual Gram inverse at one fixed Sobolev order.
Equations
- EulerTimeLpGramSobolev.gramBlockCost ι q c Rc C D = EulerParameterWordGevrey.inverseBlockCost ι q c⁻¹ Rc (3 * C ^ 2) D
Instances For
theorem
EulerTimeLpGramSobolev.gramSolution_block_gevrey
{P : Type u_1}
{U : Type u_2}
{E : Type u_3}
{ι : Type u_4}
[NormedAddCommGroup P]
[NormedSpace ℝ P]
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[CompleteSpace E]
[Fintype ι]
(directions : ι → P)
(hd : ∀ (i : ι), ‖directions i‖ ≤ 1)
(q : ℕ)
(T : ℝ)
(hT : 0 ≤ T)
(Q : P → C(↑(Set.Icc 0 T), U →L[ℝ] E))
(c : ℝ)
(hc : 0 < c)
(hLower : ∀ (x : P) (t : ↑(Set.Icc 0 T)) (v : U), c * ‖v‖ ^ 2 ≤ ‖((Q x) t) v‖ ^ 2)
(hQ : ContDiff ℝ (↑⊤) Q)
(Rc C : ℝ)
(hRc : 0 ≤ Rc)
(hC : 0 ≤ C)
(hbQ : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n Q x‖ ≤ C * EulerGevrey.majorant Rc 0 n)
(f : P → ↥(EulerTimeLp.TimeLp T U))
(hf : ContDiff ℝ (↑⊤) f)
(D R : ℝ)
(hD : 0 ≤ D)
(hR : 2 * gramBlockCost ι q c Rc C D * (EulerParameterWordGevrey.sobolevCoefficientRadius ι Rc + 1) ≤ R)
(d : ℕ)
(hbf : ∀ (n : ℕ) (x : P), EulerParameterWordGevrey.block directions q f n x ≤ D * EulerGevrey.majorant R d n)
(n : ℕ)
(x : P)
:
EulerParameterWordGevrey.block directions q (fun (y : P) => (EulerTimeLpGramInverse.gramSolver T hT (Q y) c hc ⋯) (f y))
n x ≤ EulerGevrey.majorant R (d + 1) n
One actual fixed-Hq inverse application spends one shift at the original radius, uniformly in the input grade and external derivative order.