Time integration and scale arithmetic for the centered contracts #
sd_final_time: a pointwise-in-time bound of a slice's HDot⁻¹ norm by an affine combination of
the
slice energies of three fields, with coefficients of the form produced by the centered ergodic
estimate, integrates in time and, with the scale arithmetic sd_arith_final, gives the source
right side C · ε^δ · √κ · B.
theorem
AVenhance.Infra.Section5.Contracts.sd_final_time
{f : ℝ → Homogenization.Vec 2 → ℝ}
{V : Fin 3 → ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{x y κ ν ψ B A K Cd c₀ c₁ c₂ cfl M ρ e d E : ℝ}
(hV :
∀ (j : Fin 3) (i : Fin 2),
ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => V j p.1 p.2 i) (Set.Icc 0 1 ×ˢ Set.univ))
(hpt :
∀ t ∈ Set.Ioo 0 1,
hMinusOneNorm (f t) ≤ ENNReal.ofReal
((144 * Cd * y * (c₀ * ψ * e / x) + cfl * e * ψ) * √(gradNormSq (V 0 t)) + 144 * Cd * y * (c₁ * ψ * e) * √(gradNormSq (V 1 t)) + 144 * Cd * y * (c₁ * ψ * e) * √(gradNormSq (V 2 t)) + 144 * Cd * c₂ * B * ψ * ((ρ ^ 2)⁻¹ * E)))
(hK : 1 ≤ K)
(hκ : 0 < κ)
(hν : 0 < ν)
(hνK : ν ≤ K)
(hψ : 0 ≤ ψ)
(hψκ : ψ ^ 2 ≤ K * κ * ν)
(hx : 0 < x)
(hy : 0 < y)
(hρ : 0 < ρ)
(hyx : y ≤ K * x)
(hyρ : y ≤ K * ρ)
(he : 0 ≤ e)
(hed : e ≤ d)
(hB : 0 ≤ B)
(hA : 0 ≤ A)
(hCd : 0 ≤ Cd)
(hc₀ : 0 ≤ c₀)
(hc₁ : 0 ≤ c₁)
(hc₂ : 0 ≤ c₂)
(hcfl : 0 ≤ cfl)
(hM : 0 ≤ M)
(hD₀b : √ν * √(spaceTimeGradNormSq (V 0)) ≤ A * B)
(hD₁b : √ν * √(spaceTimeGradNormSq (V 1)) ≤ A * (A / ρ) * B)
(hD₂b : √ν * √(spaceTimeGradNormSq (V 2)) ≤ A * (A / ρ) * B)
(hE : 0 ≤ E)
(hEb : (ρ ^ 2)⁻¹ * E ≤ M * d)
: