Relative residual assembly. The ten named quantitative leaves remain
explicit inputs; continuity supplies measurability and slice L2 membership.
In particular the tenth leaf is R46, not omitted from the residual.
theorem
AVenhance.Infra.Section5.RelativeError.relative_residual_of_centered_term_bounds
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(d e b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2)
(C ε δ S : ℝ)
(hResidual : ∀ t ∈ Set.Ioo 0 1, ∀ (x : Homogenization.Vec 2), residualIdentity I hΦ m κm T d e b t x)
(hContinuous :
∀ i < 10,
ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => section5Term I hΦ m κm T d e i p.1 p.2)
(Set.Ioo 0 1 ×ˢ Set.univ))
(hgroup :
∀ t ∈ Set.Ioo 0 1,
Homogenization.MeanZeroOn unitCube fun (x : Homogenization.Vec 2) =>
twistie4 I hΦ m κm T t x + twistie5 I hΦ m κm T t x + normie3 I hΦ m κm T t x)
(hterms :
∀ i < 10,
timeHMinusOneNorm (Integration.section5CenteredTerm I hΦ m κm T d e i) ≤ ENNReal.ofReal (C * √κm * ε ^ δ * S))
:
(timeHMinusOneNorm fun (t : ℝ) (x : Homogenization.Vec 2) => advDiffOp b κm (I.ansatz hΦ m κm T) t x) ≤ ENNReal.ofReal (10 * C * √κm * ε ^ δ * S)
Relative residual assembly in the centered ten-term family. Only the three grouped slots are centered; their common mean-zero identity restores the actual source residual sum.
theorem
AVenhance.Infra.Section5.RelativeError.relative_residual_of_term_bounds
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm : ℝ)
(T : ℝ → Homogenization.Vec 2 → ℝ)
(d e b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2)
(C ε δ S : ℝ)
(hResidual : ∀ t ∈ Set.Ioo 0 1, ∀ (x : Homogenization.Vec 2), residualIdentity I hΦ m κm T d e b t x)
(hContinuous :
∀ i < 10,
ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => section5Term I hΦ m κm T d e i p.1 p.2)
(Set.Ioo 0 1 ×ˢ Set.univ))
(hgroup :
∀ t ∈ Set.Ioo 0 1,
Homogenization.MeanZeroOn unitCube fun (x : Homogenization.Vec 2) =>
twistie4 I hΦ m κm T t x + twistie5 I hΦ m κm T t x + normie3 I hΦ m κm T t x)
(hcutoff1 : timeHMinusOneNorm (cutoff1 I hΦ m κm T) ≤ ENNReal.ofReal (C * √κm * ε ^ δ * S))
(htwistie1 : timeHMinusOneNorm (twistie1 I hΦ m κm T) ≤ ENNReal.ofReal (C * √κm * ε ^ δ * S))
(htwistie3 : timeHMinusOneNorm (twistie3 I hΦ m κm T) ≤ ENNReal.ofReal (C * √κm * ε ^ δ * S))
(htwistie4 :
(timeHMinusOneNorm fun (t : ℝ) => Integration.centerCell (twistie4 I hΦ m κm T t)) ≤ ENNReal.ofReal (C * √κm * ε ^ δ * S))
(htwistie5 :
(timeHMinusOneNorm fun (t : ℝ) => Integration.centerCell (twistie5 I hΦ m κm T t)) ≤ ENNReal.ofReal (C * √κm * ε ^ δ * S))
(hnormie1 : timeHMinusOneNorm (normie1 I hΦ m κm T) ≤ ENNReal.ofReal (C * √κm * ε ^ δ * S))
(hnormie2 : timeHMinusOneNorm (normie2 I hΦ m κm T) ≤ ENNReal.ofReal (C * √κm * ε ^ δ * S))
(htiny : timeHMinusOneNorm (tiny I hΦ m κm d e) ≤ ENNReal.ofReal (C * √κm * ε ^ δ * S))
(hnormie3 :
(timeHMinusOneNorm fun (t : ℝ) => Integration.centerCell (normie3 I hΦ m κm T t)) ≤ ENNReal.ofReal (C * √κm * ε ^ δ * S))
(hR46 : timeHMinusOneNorm (R46 I hΦ m κm T) ≤ ENNReal.ofReal (C * √κm * ε ^ δ * S))
:
(timeHMinusOneNorm fun (t : ℝ) (x : Homogenization.Vec 2) => advDiffOp b κm (I.ansatz hΦ m κm T) t x) ≤ ENNReal.ofReal (10 * C * √κm * ε ^ δ * S)
theorem
AVenhance.Infra.Section5.RelativeError.relative_residual_finite_and_normalized
{κ C ε δ S : ℝ}
{F : ENNReal}
(hκ : 0 < κ)
(hC : 0 ≤ C)
(hε : 0 < ε)
(hS : 0 ≤ S)
(hF : F ≤ ENNReal.ofReal (C * √κ * ε ^ δ * S))
:
A relative finite ENNReal bound supplies both finiteness and the normalized
real bound; toReal is never used on an infinite residual.