Commutator pairings of first and second order

For a smooth periodic drift b with |∂_i b_k| ≤ Lu and a smooth periodic f:

• |∑_i ∫ ∂_i f (∂_i b·∇f)| ≤ 2 Lu ∑_i ‖∂_i f‖²;
• |∑_{j,i} C_{[j,i]}| ≤ (κ/2) ‖∇³f‖² + 4 (Lu²/κ) ‖∇f‖² + 2 Lu ‖∇²f‖², where the second derivative of b is integrated by parts onto f once (this corrects the stated form of the bound).

noncomputable def AVenhance.Infra.FullTheorem.Separation.commPair (w : List (Fin 2)) (b : Homogenization.Vec 2 → Homogenization.Vec 2) (f : Homogenization.Vec 2 → ℝ) : ℝ

The commutator pairing ∫ ∂^wf (∂^w(b·∇f) - b·∇∂^wf).

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.FullTheorem.Separation.comm_one_eq {b : Homogenization.Vec 2 → Homogenization.Vec 2} {f : Homogenization.Vec 2 → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiff ℝ (↑⊤) f) (i : Fin 2) (x : Homogenization.Vec 2) : Section4.classicalWordDerivative [i] (Section4.classicalTransport b f) x - Homogenization.vecDot (b x) (spaceGrad (Section4.classicalWordDerivative [i] f) x) = ∑ k : Fin 2, spaceGrad (fun (y : Homogenization.Vec 2) => b y k) x i * spaceGrad f x k

theorem AVenhance.Infra.FullTheorem.Separation.comm_two_eq {b : Homogenization.Vec 2 → Homogenization.Vec 2} {f : Homogenization.Vec 2 → ℝ} (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiff ℝ (↑⊤) f) (j i : Fin 2) (x : Homogenization.Vec 2) : Section4.classicalWordDerivative [j, i] (Section4.classicalTransport b f) x - Homogenization.vecDot (b x) (spaceGrad (Section4.classicalWordDerivative [j, i] f) x) = ∑ k : Fin 2, (spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad (fun (z : Homogenization.Vec 2) => b z k) y i) x j * spaceGrad f x k + spaceGrad (fun (y : Homogenization.Vec 2) => b y k) x j * spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad f y k) x i + spaceGrad (fun (y : Homogenization.Vec 2) => b y k) x i * spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad f y k) x j)

theorem AVenhance.Infra.FullTheorem.Separation.commPair_nil (b : Homogenization.Vec 2 → Homogenization.Vec 2) (f : Homogenization.Vec 2 → ℝ) : commPair [] b f = 0

theorem AVenhance.Infra.FullTheorem.Separation.commPair_one_abs_le {b : Homogenization.Vec 2 → Homogenization.Vec 2} {f : Homogenization.Vec 2 → ℝ} {Lu : ℝ} (hb : ContDiff ℝ (↑⊤) b) (hf : ContDiff ℝ (↑⊤) f) (hLu : ∀ (x : Homogenization.Vec 2) (i k : Fin 2), |spaceGrad (fun (y : Homogenization.Vec 2) => b y k) x i| ≤ Lu) : |∑ i : Fin 2, commPair [i] b f| ≤ 2 * Lu * ∑ i : Fin 2, en [i] f

theorem AVenhance.Infra.FullTheorem.Separation.commPair_two_abs_le {b : Homogenization.Vec 2 → Homogenization.Vec 2} {f : Homogenization.Vec 2 → ℝ} {κ Lu : ℝ} (hκ : 0 < κ) (hb : ContDiff ℝ (↑⊤) b) (hbp : IsZ2Periodic b) (hf : ContDiff ℝ (↑⊤) f) (hfp : IsZ2Periodic f) (hLu : ∀ (x : Homogenization.Vec 2) (i k : Fin 2), |spaceGrad (fun (y : Homogenization.Vec 2) => b y k) x i| ≤ Lu) : |∑ j : Fin 2, ∑ i : Fin 2, commPair [j, i] b f| ≤ κ / 2 * ∑ l : Fin 2, ∑ j : Fin 2, ∑ i : Fin 2, en [l, j, i] f + 4 * (Lu ^ 2 / κ) * ∑ k : Fin 2, en [k] f + 2 * Lu * ∑ j : Fin 2, ∑ i : Fin 2, en [j, i] f