Splitting a centered term into its nondivergence part and a divergence

theorem AVenhance.Infra.Section5.Contracts.sd_integral_vecDiv_eq_zero {F : Homogenization.Vec 2 → Homogenization.Vec 2} (hF : ContDiff ℝ (↑⊤) F) (hp : IsZ2Periodic F) : ∫ (x : Homogenization.Vec 2) in unitCube, vecDiv F x = 0

The mean of the divergence of a smooth periodic field over the unit cube vanishes.

theorem AVenhance.Infra.Section5.Contracts.sd_vecDiv_continuous {F : Homogenization.Vec 2 → Homogenization.Vec 2} (hF : ContDiff ℝ (↑⊤) F) : Continuous (vecDiv F)

theorem AVenhance.Infra.Section5.Contracts.sd_centered_split_bound {tw Nd : Homogenization.Vec 2 → ℝ} {F : Homogenization.Vec 2 → Homogenization.Vec 2} (hNd : Continuous Nd) (hF : ContDiff ℝ (↑⊤) F) (hp : IsZ2Periodic F) (h : ∀ (x : Homogenization.Vec 2), tw x = Nd x - vecDiv F x) : hMinusOneNorm (Integration.centerCell tw) ≤ hMinusOneNorm (Integration.centerCell Nd) + ENNReal.ofReal √(gradNormSq F)

Centered split: if tw = Nd - div F with Nd continuous and F smooth periodic, then ‖center tw‖_{HDot⁻¹} ≤ ‖center Nd‖_{HDot⁻¹} + ‖F‖_{L²}.

theorem AVenhance.Infra.Section5.Contracts.sd_centered_div_bound {tw : Homogenization.Vec 2 → ℝ} {F : Homogenization.Vec 2 → Homogenization.Vec 2} (hF : ContDiff ℝ (↑⊤) F) (hp : IsZ2Periodic F) (h : ∀ (x : Homogenization.Vec 2), tw x = -vecDiv F x) : hMinusOneNorm (Integration.centerCell tw) ≤ ENNReal.ofReal √(gradNormSq F)

Centered divergence bound (slots twistie4, twistie5): a pure divergence tw = -div F of a smooth periodic flux has mean zero, so ‖center tw‖_{HDot⁻¹} ≤ ‖F‖_{L²}.

theorem AVenhance.Infra.Section5.Contracts.sd_gradNormSq_le {F V : Homogenization.Vec 2 → Homogenization.Vec 2} (hF : Continuous F) (hV : Continuous V) {c : ℝ} (h : ∀ (x : Homogenization.Vec 2), Homogenization.vecNormSq (F x) ≤ c ^ 2 * Homogenization.vecNormSq (V x)) : gradNormSq F ≤ c ^ 2 * gradNormSq V

The L² norm of a field bounded pointwise by a multiple of another one.

theorem AVenhance.Infra.Section5.Contracts.sd_sqrt_comb_le {k₀ k₁ g₀ g₁ g₂ : ℝ} (hk₀ : 0 ≤ k₀) (hk₁ : 0 ≤ k₁) (h₀ : 0 ≤ g₀) (h₁ : 0 ≤ g₁) (h₂ : 0 ≤ g₂) : √(k₀ ^ 2 * g₀ + k₁ ^ 2 * (g₁ + g₂)) ≤ k₀ * √g₀ + k₁ * √g₁ + k₁ * √g₂