Coefficient-only Sobolev costs for the actual acceleration right side.
def
EulerParameterWordGevrey.accelerationBlockAmplitude
(ι : Type u_1)
[Fintype ι]
(q : ℕ)
(Rc CA CB Cf Cv : ℝ)
:
Acceleration block amplitude, given by 3*sobolevCoefficientAmplitude ι q Rc CA * (Cf+6*sobolevCoefficientAmplitude ι q Rc CB*Cv).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
EulerParameterWordGevrey.block_acceleration_forcing_of_tensor
{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)
(hd : ∀ (i : ι), ‖directions i‖ ≤ 1)
(q : ℕ)
(A : P → E →L[ℝ] F)
(B : P → G →L[ℝ] E)
(f : P → E)
(v : P → G)
(hA : ContDiff ℝ (↑⊤) A)
(hB : ContDiff ℝ (↑⊤) B)
(hf : ContDiff ℝ (↑⊤) f)
(hv : ContDiff ℝ (↑⊤) v)
(Rc R CA CB Cf Cv : ℝ)
(hRc : 0 ≤ Rc)
(hRcR : sobolevCoefficientRadius ι Rc ≤ R)
(hCA : 0 ≤ CA)
(hCB : 0 ≤ CB)
(hCf : 0 ≤ Cf)
(hCv : 0 ≤ Cv)
(hbA : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n A x‖ ≤ CA * EulerGevrey.majorant Rc 0 n)
(hbB : ∀ (n : ℕ) (x : P), ‖iteratedFDeriv ℝ n B x‖ ≤ CB * EulerGevrey.majorant Rc 0 n)
(d : ℕ)
(hbf : ∀ (n : ℕ) (x : P), block directions q f n x ≤ Cf * EulerGevrey.majorant R d n)
(hbv : ∀ (n : ℕ) (x : P), block directions q v n x ≤ Cv * EulerGevrey.majorant R d n)
(n : ℕ)
(x : P)
:
block directions q (fun (y : P) => (A y) (f y - 2 • (B y) (v y))) n x ≤ accelerationBlockAmplitude ι q Rc CA CB Cf Cv * EulerGevrey.majorant R d n
Only coefficient tensors are converted to fixed Sobolev blocks. Neither the forcing nor velocity radius changes.