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