test duality for the additional divergence-form residual.
This module proves the HDot⁻¹ step needed for R46. The source does not provide
the L² estimate on its flux; that independent coefficient estimate remains an
input to the big-bound estimate argument.
noncomputable def
AVenhance.Infra.Section5.r46Flux
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(t : ℝ)
(x : Homogenization.Vec 2)
:
The vector field whose divergence is the transition-window residual.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AVenhance.Infra.Section5.R46_eq_cellDivergence
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(t : ℝ)
:
Pointwise, R46 is exactly the divergence of its transition-window flux.
theorem
AVenhance.Infra.Section5.hMinusOneNorm_R46_le
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(t : ℝ)
(hF : ContDiff ℝ (↑⊤) (r46Flux I hΦ m κm T t))
(hper : IsZ2Periodic (r46Flux I hΦ m κm T t))
:
The HDot⁻¹ norm of R46 is controlled by the spatial L² norm of its
flux. This is the exact divergence-duality step; it does not assert the
source-missing estimate of that flux in terms of κ, ε, and θ₀.
theorem
AVenhance.Infra.Section5.timeHMinusOneNorm_R46_le
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(hF : ∀ t ∈ Set.Ioo 0 1, ContDiff ℝ (↑⊤) (r46Flux I hΦ m κm T t))
(hper : ∀ t ∈ Set.Ioo 0 1, IsZ2Periodic (r46Flux I hΦ m κm T t))
:
(timeHMinusOneNorm fun (t : ℝ) => R46 I hΦ m κm T t) ≤ (∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal √(gradNormSq (r46Flux I hΦ m κm T t)) ^ 2) ^ (1 / 2)
Time-integrated divergence duality for R46 in the exact BigBound carrier.
The right side is the space-time L² flux norm, expressed as a lower integral.