with the actual initial corrector. The active flow derivative bound, corrector size and positive initial gradient trace are separate named inputs. No identity ansatz(0)=g is asserted.
theorem
AVenhance.Infra.Section5.RelativeError.RelativeInitial.abs_coord_le_sqrt_vecNormSq
(v : Homogenization.Vec 2)
(i : Fin 2)
:
theorem
AVenhance.Infra.Section5.RelativeError.relative_flowGrad_entry_le_two
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(l : ℤ)
(hDX : ∀ (y : Homogenization.Vec 2), ‖fderiv ℝ (I.xFlow hΦ m l 0) y‖ ≤ 2)
(x : Homogenization.Vec 2)
(i j : Fin 2)
:
The active-flow operator bound used by implies the entrywise bound in the derivative-row convention.
theorem
AVenhance.Infra.Section5.RelativeError.relative_initial_corrector_bound
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κ : ℝ)
{g : Homogenization.Vec 2 → ℝ}
(hg : ContDiff ℝ (↑⊤) g)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(hT0 : T 0 = g)
{B K : ℝ}
(hB : 0 ≤ B)
(hK : 0 ≤ K)
(hChi : ∀ (k : ℤ), I.xiMK m k 0 ≠ 0 → ∀ (x : Homogenization.Vec 2) (i : Fin 2), |I.chiTilde hΦ m κ k 0 x i| ≤ B)
(hFlow2 :
∀ (k : ℤ),
I.xiMK m k 0 ≠ 0 → ∀ (x : Homogenization.Vec 2) (i j : Fin 2), |I.flowGrad hΦ m (lIdx β I.Λ m k) 0 x i j| ≤ 2)
(hCutoff : ∑ k ∈ ⋯.toFinset, |I.xiMK m k 0| ≤ K)
:
The initial corrector series has only the positive derivative of g. The two-dimensional conversion costs 8 with entrywise |DX|<=2.