The forced energy estimate on the open time half-line

forced_energy_estimate_Ioi: the energy estimate of Energy/Estimate for a comparison function v that is jointly C² only on (0,∞) × ℝ², with the initial defect controlled from the right, √‖u(s) - v(s)‖² ≤ D for s → 0⁺. Proof: the integrated energy bound on [s,t] (PartIEnergyIoiBound), then s → 0⁺ along the eventual set where the initial bound holds, using monotone convergence for the space-time gradient energy.

def AVenhance.Infra.Section5.Integration.EnergyIoi.PartIEnergyIoi.closedCube : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Section5.Integration.EnergyIoi.PartIEnergyIoi.closedCube = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Section5.Integration.EnergyIoi.PartIEnergyIoi.isCompact_closedCube : IsCompact closedCube

theorem AVenhance.Infra.Section5.Integration.EnergyIoi.PartIEnergyIoi.unitCube_subset_closedCube : unitCube ⊆ closedCube

theorem AVenhance.Infra.Section5.Integration.EnergyIoi.PartIEnergyIoi.continuous_vecNormSq_two' : Continuous fun (v : Homogenization.Vec 2) => Homogenization.vecNormSq v

theorem AVenhance.Infra.Section5.Integration.EnergyIoi.setIntegral_Ioo_prod_unitCube {V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {a : ℝ} (hab : a ≤ 1) (hV : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => V p.1 p.2) (Set.Icc a 1 ×ˢ Set.univ)) : ∫ (p : ℝ × Homogenization.Vec 2) in Set.Ioo a 1 ×ˢ unitCube, Homogenization.vecNormSq (V p.1 p.2) = ∫ (t : ℝ) in a..1, ∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecNormSq (V t x)

The space-time energy over (a,1) × cube as an iterated integral, for a field continuous on [a,1] × ℝ².

theorem AVenhance.Infra.Section5.Integration.EnergyIoi.IoiSetup.errGrad_jointContinuousOn {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : IoiSetup φ κ θ₀ u v) {a : ℝ} (ha : 0 < a) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (u p.1) p.2 - spaceGrad (v p.1) p.2) (Set.Ici a ×ˢ Set.univ)

The joint error gradient is continuous on [a,∞) × ℝ² for a > 0.

theorem AVenhance.Infra.Section5.Integration.EnergyIoi.IoiSetup.energy_bound_of_init {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : IoiSetup φ κ θ₀ u v) (hfin : (timeHMinusOneNorm fun (s : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel φ) κ v s x) ≠ ⊤) {D s τ : ℝ} (hs : 0 < s) (hsτ : s ≤ τ) (hτ : τ ≤ 1) (hD : √(l2NormSq fun (x : Homogenization.Vec 2) => u s x - v s x) ≤ D) : (l2NormSq fun (x : Homogenization.Vec 2) => u τ x - v τ x) + κ * ∫ (r : ℝ) in s..τ, Energy.errGrad u v r ≤ D ^ 2 + (timeHMinusOneNorm fun (s : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel φ) κ v s x).toReal ^ 2 / κ

Energy bound from the initial bound at a small positive time.

theorem AVenhance.Infra.Section5.Integration.EnergyIoi.IoiSetup.spaceTimeGradNormSq_bound {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : IoiSetup φ κ θ₀ u v) (hfin : (timeHMinusOneNorm fun (s : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel φ) κ v s x) ≠ ⊤) {D : ℝ} (hinit : ∀ᶠ (s : ℝ) in nhdsWithin 0 (Set.Ioi 0), √(l2NormSq fun (x : Homogenization.Vec 2) => u s x - v s x) ≤ D) : (κ * spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (u s) x - spaceGrad (v s) x) ≤ D ^ 2 + (timeHMinusOneNorm fun (s : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel φ) κ v s x).toReal ^ 2 / κ

The space-time gradient energy, as s → 0⁺.

theorem AVenhance.Infra.Section5.Integration.forced_energy_estimate_Ioi {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsAdmissibleStream φ) {κ : ℝ} (hκ : 0 < κ) {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (hu : IsClassicalSol (streamVel φ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ u) (hv : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => v p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)) (hvs : ∀ (t : ℝ), 0 < t → ContDiff ℝ (↑⊤) (v t)) (hvp : ∀ (t : ℝ), 0 < t → IsZ2Periodic (v t)) (hfin : (timeHMinusOneNorm fun (s : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel φ) κ v s x) ≠ ⊤) {D : ℝ} (hinit : ∀ᶠ (s : ℝ) in nhdsWithin 0 (Set.Ioi 0), √(l2NormSq fun (x : Homogenization.Vec 2) => u s x - v s x) ≤ D) (t : ℝ) : t ∈ Set.Ioc 0 1 → √(l2NormSq fun (x : Homogenization.Vec 2) => u t x - v t x) + √κ * √(spaceTimeGradNormSq fun (s : ℝ) (x : Homogenization.Vec 2) => spaceGrad (u s) x - spaceGrad (v s) x) ≤ 2 * (D + (timeHMinusOneNorm fun (s : ℝ) (x : Homogenization.Vec 2) => advDiffOp (streamVel φ) κ v s x).toReal / √κ)

The forced energy estimate on the open time half-line: v need only be jointly C² on (0,∞) × ℝ², and the initial defect is controlled from the right (s → 0⁺).