The exact algebraic split and HDot⁻¹ estimate for tiny.

The component L² bounds and the mean-zero condition for the nondivergence component are hypotheses here; the mean-zero condition is proved in Contracts/MeanZero.lean.

noncomputable def AVenhance.Infra.Section5.tinyNondivergencePart {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) : ℝ

The nondivergence summand in the definition of tiny.

Equations

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

theorem AVenhance.Infra.Section5.tiny_eq_divergence_add_nondivergence {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (d e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) : tiny I hΦ m κm d e t = fun (x : Homogenization.Vec 2) => vecDiv (fun (y : Homogenization.Vec 2) => d t y + e t y) x + tinyNondivergencePart I hΦ m κm e t x

tiny is its divergence part plus the scalar nondivergence remainder.

theorem AVenhance.Infra.Section5.hMinusOneNorm_tiny_le_of_components {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (d e : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (hdivL2 : Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => vecDiv (fun (y : Homogenization.Vec 2) => d t y + e t y) x) (hN_L2 : Homogenization.MemL2On unitCube (tinyNondivergencePart I hΦ m κm e t)) (hN_mean : Homogenization.MeanZeroOn unitCube (tinyNondivergencePart I hΦ m κm e t)) (hF : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => d t x + e t x) (hFper : IsZ2Periodic fun (x : Homogenization.Vec 2) => d t x + e t x) : hMinusOneNorm (tiny I hΦ m κm d e t) ≤ ENNReal.ofReal √(gradNormSq fun (x : Homogenization.Vec 2) => d t x + e t x) + ENNReal.ofReal ((2 * Real.pi)⁻¹ * √(l2NormSq (tinyNondivergencePart I hΦ m κm e t)))

Conditional HDot⁻¹ estimate for the complete tiny term. The two component L² premises are the analytic estimates proved from e.dm.bounds and e.Em-1.thetam; the mean-zero premise is a hypothesis here and is proved in Contracts/MeanZero.lean.