Positive-time Hmr gradient source reductions. Differentiation is needed only on the physical time support of the measure. The owner modules are imported; their global regularity interfaces are not changed.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_hmr_gradient_spatial_sum {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) (t : ℝ) (hD1 : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t y i j k) x) (hD2 : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2) (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t x i j k) y i) x) (x : Homogenization.Vec 2) (p : Fin 2) : spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r t x) x p = ∑ i : Fin 2, ∑ n ∈ Finset.range (Nstar β), ∑ j : Fin 2, ∑ k : Fin 2, spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t x i j k) y i) x p * I.qMNR κ m n (r + 1) t j k

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_hmr_gradient_components_L2 {β C₀ A : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) {μ : MeasureTheory.Measure (ℝ × Homogenization.Vec 2)} (hμ : μ.AbsolutelyContinuous (MeasureTheory.volume.restrict (Set.Ioi 0 ×ˢ Set.univ))) (hcutoff : I.Czeta ≤ C₀) (hm : 1 ≤ m) (hκ : 0 < κ) (hA : 0 ≤ A) (hratio : epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m) ≤ 1) (hAmnrHess : ∀ n ∈ Finset.range (Nstar β), MeasureTheory.eLpNorm (Section4.amnrSpatialDivergenceGradientTensor I hΦ m κ T n r) 2 μ ≤ ENNReal.ofReal A) (hHessEntryMeas : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k p : Fin 2), MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => Section4.amnrSpatialDivergenceGradientTensor I hΦ m κ T n r z i j k p) μ) (hD1 : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2) (t : ℝ), 0 < t → ∀ (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t y i j k) x) (hD2 : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2) (t : ℝ), 0 < t → ∀ (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t x i j k) y i) x) (p : Fin 2) : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r z.1 x) z.2 p) 2 μ ≤ 8 * ↑(Nstar β) * ENNReal.ofReal (Section4.hmrGradientQbase I C₀ m r * A)

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_hmr_gradient_L2 {β C₀ A : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) {μ : MeasureTheory.Measure (ℝ × Homogenization.Vec 2)} (hμ : μ.AbsolutelyContinuous (MeasureTheory.volume.restrict (Set.Ioi 0 ×ˢ Set.univ))) (hcutoff : I.Czeta ≤ C₀) (hm : 1 ≤ m) (hκ : 0 < κ) (hA : 0 ≤ A) (hratio : epsilon β I.Λ m ^ 2 / (κ * tau β I.Λ m) ≤ 1) (hAmnrHess : ∀ n ∈ Finset.range (Nstar β), MeasureTheory.eLpNorm (Section4.amnrSpatialDivergenceGradientTensor I hΦ m κ T n r) 2 μ ≤ ENNReal.ofReal A) (hHessEntryMeas : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k p : Fin 2), MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => Section4.amnrSpatialDivergenceGradientTensor I hΦ m κ T n r z i j k p) μ) (hGradientMeas : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r z.1 x) z.2) μ) (hD1 : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2) (t : ℝ), 0 < t → ∀ (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t y i j k) x) (hD2 : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2) (t : ℝ), 0 < t → ∀ (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Amnr hΦ m κ n T r t x i j k) y i) x) : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r z.1 x) z.2) 2 μ ≤ ENNReal.ofReal (16 * ↑(Nstar β) * A * Section4.hmrGradientQbase I C₀ m r)

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_Hm_gradient_spatial_sum {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (hD : ∀ r ∈ Finset.range (Jcut β), ∀ (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Hmr hΦ m κ T r t y) x) : (spaceGrad fun (x : Homogenization.Vec 2) => I.Hm hΦ m κ T t x) = ∑ r ∈ Finset.range (Jcut β), spaceGrad fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r t x

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_Hm_gradient_L2_sum_positive {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (hD : ∀ r ∈ Finset.range (Jcut β), ∀ (t : ℝ), 0 < t → ∀ (x : Homogenization.Vec 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => I.Hmr hΦ m κ T r t y) x) {B : ℕ → ℝ} (hB : ∀ (r : ℕ), 0 ≤ B r) (hterm : ∀ r ∈ Finset.range (Jcut β), MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hmr hΦ m κ T r z.1 x) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (B r)) : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (fun (x : Homogenization.Vec 2) => I.Hm hΦ m κ T z.1 x) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (∑ r ∈ Finset.range (Jcut β), B r)