Pointwise bound for the corrector part of the ansatz

Source: enhance.tex (e.tildethetam.to.Tm.A.temptemp). At a fixed time t, θTilde_m - T_{m-1} - HTilde_m = ∑_{k odd} ξ_{m,k} ΧTilde_{m,k} · G_{l_k} is bounded pointwise by 4 ‖Χ‖_∞ (|∂₁T| + |∂₂T|): G_{l_k} = (∇X ∘ X⁻¹)∇T with |(∇X∘X⁻¹)_{ij}| ≤ 2 on supp ξ_{m,k}, and ∑_k ξ_{m,k} = 1, 0 ≤ ξ_{m,k}.

theorem AVenhance.Infra.Section5.Integration.vecDot_mulVec_abs_le {χ g : Homogenization.Vec 2} {F : Matrix (Fin 2) (Fin 2) ℝ} {c : ℝ} (hc : 0 ≤ c) (hχ : ∀ (j : Fin 2), |χ j| ≤ c) (hF : ∀ (i j : Fin 2), |F i j| ≤ 2) : |Homogenization.vecDot χ (F.mulVec g)| ≤ 4 * c * (|g 0| + |g 1|)

A bilinear pairing of a bounded vector with a matrix-vector product of entrywise bound 2.

noncomputable def AVenhance.Infra.Section5.Integration.chiSup {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) : ℝ

The sup norm of the corrector Χ_{m,k}, in the form of CorrectorBounds.

Equations

• AVenhance.Infra.Section5.Integration.chiSup I κ m = (4 * Real.pi ^ 2 * κ / AVenhance.epsilon β I.Λ m ^ 2)⁻¹ * |2 * Real.pi * AVenhance.a β I.Λ m * AVenhance.epsilon β I.Λ m|

theorem AVenhance.Infra.Section5.Integration.chiSup_nonneg {β : ℝ} (I : Ingredients β) {κ : ℝ} (hκ : 0 < κ) (m : ℕ) : 0 ≤ chiSup I κ m

theorem AVenhance.Infra.Section5.Integration.flowGrad_abs_le_two {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) (k : ℤ) {t : ℝ} (hξ : I.xiMK m k t ≠ 0) (x : Homogenization.Vec 2) (i j : Fin 2) : |I.flowGrad hΦ m (lIdx β I.Λ m k) t x i j| ≤ 2

Entries of the flow gradient are bounded by 2 on supp ξ_{m,k}.

theorem AVenhance.Infra.Section5.Integration.ansatzPairing_abs_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {κm : ℝ} (hκ : 0 < κm) {T : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (k : ℤ) (hξ : I.xiMK m k t ≠ 0) (x : Homogenization.Vec 2) : |RelativeError.ansatzPairing I hΦ m κm T k t x| ≤ 4 * chiSup I κm m * (|spaceGrad (T t) x 0| + |spaceGrad (T t) x 1|)

Pointwise bound on one pairing ΧTilde_{m,k} · G_{l_k} on supp ξ_{m,k}.

theorem AVenhance.Infra.Section5.Integration.ansatz_sub_T_sub_Hm_abs_le {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {κm : ℝ} (hκ : 0 < κm) {T : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} (hTt : ContDiff ℝ (↑⊤) (T t)) (x : Homogenization.Vec 2) : |I.ansatz hΦ m κm T t x - T t x - I.Hm hΦ m κm T t x| ≤ 4 * chiSup I κm m * (|spaceGrad (T t) x 0| + |spaceGrad (T t) x 1|)

Pointwise bound for the corrector part of the ansatz at a fixed time.