The mean forcing coefficient in the actual diffusivity chain.
theorem
AVenhance.Infra.Section4.iterate_previous_diffusivity_eq
{β : ℝ}
(I : Ingredients β)
(κ : ℝ)
{m M : ℕ}
(hm : 1 ≤ m)
(hmM : m ≤ M)
:
The physical preceding diffusivity is exactly the scalar homogenized coefficient, by the recursion rather than a comparison hypothesis.
theorem
AVenhance.Infra.Section4.iterate_mean_coefficient_bound
{β : ℝ}
(I : Ingredients β)
(κ : ℝ)
{m M : ℕ}
(hm : 1 ≤ m)
(hmM : m ≤ M)
(hκ : 0 < I.kappaAt κ m (M - m))
(hcondition : epsilon β I.Λ m ^ 2 ≤ I.kappaAt κ m (M - m) * tau β I.Λ m / 2)
:
‖timeAvgMat (I.Kmat (I.kappaAt κ m (M - m)) m) - I.kappaAt κ (m - 1) (M - (m - 1)) • 1‖ ≤ a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / I.kappaAt κ m (M - m) * (4 * Real.pi ^ 2 * I.Czeta * ↑(Nstar β) * 2 ^ Nstar β * (epsilon β I.Λ m ^ 2 / (I.kappaAt κ m (M - m) * tau β I.Λ m)) ^ Nstar β + 2 * ↑(Nstar β) * I.Czeta * ↑(Nstar β).factorial * 2 ^ Nstar β * 2 ^ Nstar β * I.Chat ^ 2 * 8 ^ Nstar β * (tau β I.Λ m / tauP β I.Λ m) ^ Nstar β)
The mean forcing error retains both finite-averaging errors from E21c.
noncomputable def
AVenhance.Infra.Section4.iterateMeanErrorBound
{β : ℝ}
(I : Ingredients β)
(κm : ℝ)
(m : ℕ)
:
The explicit two-error coefficient from the finite average comparison.
Equations
- One or more equations did not get rendered due to their size.