HDot⁻¹ duality estimate for the divergence-form term normie2.
noncomputable def
AVenhance.Infra.Section5.normie2Flux
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(t : ℝ)
(x : Homogenization.Vec 2)
:
Vector flux under the divergence in normie2.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AVenhance.Infra.Section5.timeHMinusOneNorm_normie2_le
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(hF : ∀ t ∈ Set.Ioo 0 1, ContDiff ℝ (↑⊤) (normie2Flux I hΦ m κm T t))
(hper : ∀ t ∈ Set.Ioo 0 1, IsZ2Periodic (normie2Flux I hΦ m κm T t))
:
(timeHMinusOneNorm fun (t : ℝ) => normie2 I hΦ m κm T t) ≤ (∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal √(gradNormSq (normie2Flux I hΦ m κm T t)) ^ 2) ^ (1 / 2)
Time-integrated HDot⁻¹ estimate for normie2.