Torus calculus for the separation estimates

Integral helpers over the unit cube, a coordinate integration by parts for smooth periodic functions (deduced from theta_divergence_pairing), and the integration-by-parts identity that removes the second derivative of the drift from the second-order commutator pairing.

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

∫_{cell} (∂^w f)².

Equations

• AVenhance.Infra.FullTheorem.Separation.en w f = ∫ (x : Homogenization.Vec 2) in AVenhance.unitCube, AVenhance.Infra.Section4.classicalWordDerivative w f x ^ 2

theorem AVenhance.Infra.FullTheorem.Separation.intOn {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f unitCube MeasureTheory.volume

theorem AVenhance.Infra.FullTheorem.Separation.abs_integral_le_of {F q : Homogenization.Vec 2 → ℝ} (hF : Continuous F) (hq : Continuous q) (h : ∀ (x : Homogenization.Vec 2), |F x| ≤ q x) : |∫ (x : Homogenization.Vec 2) in unitCube, F x| ≤ ∫ (x : Homogenization.Vec 2) in unitCube, q x

theorem AVenhance.Infra.FullTheorem.Separation.int_sum2 {φ : Fin 2 → Homogenization.Vec 2 → ℝ} (h : ∀ (i : Fin 2), Continuous (φ i)) : ∫ (x : Homogenization.Vec 2) in unitCube, ∑ i : Fin 2, φ i x = ∑ i : Fin 2, ∫ (x : Homogenization.Vec 2) in unitCube, φ i x

theorem AVenhance.Infra.FullTheorem.Separation.int_sum_sum {φ : Fin 2 → Fin 2 → Homogenization.Vec 2 → ℝ} (h : ∀ (i j : Fin 2), Continuous (φ i j)) : ∫ (x : Homogenization.Vec 2) in unitCube, ∑ i : Fin 2, ∑ j : Fin 2, φ i j x = ∑ i : Fin 2, ∑ j : Fin 2, ∫ (x : Homogenization.Vec 2) in unitCube, φ i j x

theorem AVenhance.Infra.FullTheorem.Separation.int_sum_sum_sum {φ : Fin 2 → Fin 2 → Fin 2 → Homogenization.Vec 2 → ℝ} (h : ∀ (i j k : Fin 2), Continuous (φ i j k)) : ∫ (x : Homogenization.Vec 2) in unitCube, ∑ i : Fin 2, ∑ j : Fin 2, ∑ k : Fin 2, φ i j k x = ∑ i : Fin 2, ∑ j : Fin 2, ∑ k : Fin 2, ∫ (x : Homogenization.Vec 2) in unitCube, φ i j k x

theorem AVenhance.Infra.FullTheorem.Separation.contDiff_word (w : List (Fin 2)) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (Section4.classicalWordDerivative w f)

theorem AVenhance.Infra.FullTheorem.Separation.cont_word (w : List (Fin 2)) {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) : Continuous (Section4.classicalWordDerivative w f)

theorem AVenhance.Infra.FullTheorem.Separation.ibp_coord {g h : Homogenization.Vec 2 → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hh : ContDiff ℝ (↑⊤) h) (hgp : IsZ2Periodic g) (hhp : IsZ2Periodic h) (j : Fin 2) : ∫ (x : Homogenization.Vec 2) in unitCube, g x * spaceGrad h x j = -∫ (x : Homogenization.Vec 2) in unitCube, spaceGrad g x j * h x

Coordinate integration by parts for smooth periodic functions.

theorem AVenhance.Infra.FullTheorem.Separation.triple_identity {F2 Fk mik mjk Fik : Homogenization.Vec 2 → ℝ} (hF2 : ContDiff ℝ (↑⊤) F2) (hFk : ContDiff ℝ (↑⊤) Fk) (hm : ContDiff ℝ (↑⊤) mik) (hF2p : IsZ2Periodic F2) (hFkp : IsZ2Periodic Fk) (hmp : IsZ2Periodic mik) (hmjk : Continuous mjk) (hFik : Continuous Fik) (j : Fin 2) : ∫ (x : Homogenization.Vec 2) in unitCube, F2 x * (spaceGrad mik x j * Fk x + mjk x * Fik x + mik x * spaceGrad Fk x j) = ∫ (x : Homogenization.Vec 2) in unitCube, -(mik x * spaceGrad F2 x j * Fk x) + F2 x * mjk x * Fik x

The integration-by-parts identity of the second-order commutator pairing: only first derivatives of the drift survive.