Open-time HTilde_m gradient: componentwise estimates

Copies of the HmBounds gradient lemmas in which the spatial differentiability premises are required only for t > 0 (the iterates' Amnr recursion reads the arbitrary negative-time extension of T at t ≤ 0). The pointwise funext identities become a.e. identities with respect to a measure carried on {z | 0 < z.1}.

theorem AVenhance.Infra.Section5.RelativeError.hmr_spaceGrad_eq_second_spatial_derivative_sum_at {β : ℝ} (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

Differentiate the exact Hmr expansion once more in space. This is the source identity behind the (k,ell)=(2,0) instance of p.Amnr.

theorem AVenhance.Infra.Section5.RelativeError.hmr_spaceGrad_components_eLpNorm_le_of_pAmnr_qMNR_Ioi {β C₀ A : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) {μ : MeasureTheory.Measure (ℝ × Homogenization.Vec 2)} (hμ : ∀ᵐ (z : ℝ × Homogenization.Vec 2) ∂μ, 0 < z.1) (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)

Each output component of the gradient is bounded by the finite (i,n,j,k) sum supplied by the (k,ell)=(2,0) AMNR estimate.

theorem AVenhance.Infra.Section5.RelativeError.hmr_spaceGrad_eLpNorm_le_of_pAmnr_qMNR_Ioi {β C₀ A : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (r : ℕ) {μ : MeasureTheory.Measure (ℝ × Homogenization.Vec 2)} (hμ : ∀ᵐ (z : ℝ × Homogenization.Vec 2) ∂μ, 0 < z.1) (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)

Open-time vector-valued ∇Hmr bound from the AMNR tensor bound.

theorem AVenhance.Infra.Section5.RelativeError.hm_spaceGrad_eq_sum_hmr_at {β : ℝ} (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

Differentiation in x commutes with the finite Hm sum.

theorem AVenhance.Infra.Section5.RelativeError.hm_gradient_eLpNorm_le_sum_of_hmr_Ioi {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) {μ : MeasureTheory.Measure (ℝ × Homogenization.Vec 2)} (hμ : ∀ᵐ (z : ℝ × Homogenization.Vec 2) ∂μ, 0 < z.1) (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 μ ≤ 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 μ ≤ ENNReal.ofReal (∑ r ∈ Finset.range (Jcut β), B r)

Open-time sum over r < Jcut β of the termwise ∇Hmr bounds.