Time cutoff reducing the open half-line energy setup to ForcedSetup

The forced energy estimate (Energy/*) is stated for a comparison function v that is jointly C² on the closed half-line [0,∞) × ℝ². For the ansatz θTilde_m this fails at t = 0. Here v is only jointly C² on (0,∞) × ℝ². For s > 0, multiplying v by a smooth time cutoff that vanishes on t ≤ s/3 and equals 1 on t ≥ s/2 gives a function cutoffV s v satisfying all the hypotheses of ForcedSetup and agreeing with v on [s/2, ∞); every pointwise-in-time statement of the Energy development at times ≥ s then transfers to v.

structure AVenhance.Infra.Section5.Integration.EnergyIoi.IoiSetup (φ : ℝ → Homogenization.Vec 2 → ℝ) (κ : ℝ) (θ₀ : Homogenization.Vec 2 → ℝ) (u v : ℝ → Homogenization.Vec 2 → ℝ) : Prop

Standing hypotheses of the open half-line forced energy estimate.

• hφ : IsAdmissibleStream φ
• hκ : 0 < κ
• 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)

noncomputable def AVenhance.Infra.Section5.Integration.EnergyIoi.cutoffTime (s t : ℝ) : ℝ

The time cutoff: 0 on t ≤ s/3, 1 on t ≥ s/2.

Equations

• AVenhance.Infra.Section5.Integration.EnergyIoi.cutoffTime s t = ((t - s / 3) * (6 / s)).smoothTransition

noncomputable def AVenhance.Infra.Section5.Integration.EnergyIoi.cutoffV (s : ℝ) (v : ℝ → Homogenization.Vec 2 → ℝ) : ℝ → Homogenization.Vec 2 → ℝ

The cut-off comparison function.

Equations

• AVenhance.Infra.Section5.Integration.EnergyIoi.cutoffV s v t x = AVenhance.Infra.Section5.Integration.EnergyIoi.cutoffTime s t * v t x

theorem AVenhance.Infra.Section5.Integration.EnergyIoi.cutoffTime_eq_one {s t : ℝ} (hs : 0 < s) (ht : s / 2 ≤ t) : cutoffTime s t = 1

theorem AVenhance.Infra.Section5.Integration.EnergyIoi.cutoffTime_eq_zero {s t : ℝ} (hs : 0 < s) (ht : t ≤ s / 3) : cutoffTime s t = 0

theorem AVenhance.Infra.Section5.Integration.EnergyIoi.cutoffTime_contDiff (s : ℝ) : ContDiff ℝ (↑⊤) (cutoffTime s)

theorem AVenhance.Infra.Section5.Integration.EnergyIoi.cutoffV_slice_eq {s : ℝ} (hs : 0 < s) (v : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (ht : s / 2 ≤ t) : cutoffV s v t = v t

The cut-off function agrees with v on [s/2, ∞), as a function of space.

theorem AVenhance.Infra.Section5.Integration.EnergyIoi.cutoffV_slice_zero {s : ℝ} (hs : 0 < s) (v : ℝ → Homogenization.Vec 2 → ℝ) {t : ℝ} (ht : t ≤ 0) : cutoffV s v t = fun (x : Homogenization.Vec 2) => 0

theorem AVenhance.Infra.Section5.Integration.EnergyIoi.cutoffV_contDiff {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : IoiSetup φ κ θ₀ u v) {s : ℝ} (hs : 0 < s) : ContDiff ℝ 2 fun (p : ℝ × Homogenization.Vec 2) => cutoffV s v p.1 p.2

theorem AVenhance.Infra.Section5.Integration.EnergyIoi.IoiSetup.cutoff {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : IoiSetup φ κ θ₀ u v) {s : ℝ} (hs : 0 < s) : Energy.ForcedSetup φ κ θ₀ u (cutoffV s v)

The cut-off function satisfies the hypotheses of the closed half-line energy estimate.

theorem AVenhance.Infra.Section5.Integration.EnergyIoi.advDiffOp_cutoffV (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (κ : ℝ) {s : ℝ} (hs : 0 < s) (v : ℝ → Homogenization.Vec 2 → ℝ) {r : ℝ} (hr : s / 2 < r) (x : Homogenization.Vec 2) : advDiffOp b κ (cutoffV s v) r x = advDiffOp b κ v r x

The defect of the cut-off function agrees with that of v for t > s/2.

theorem AVenhance.Infra.Section5.Integration.EnergyIoi.advDiffOp_cutoffV_slice (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (κ : ℝ) {s : ℝ} (hs : 0 < s) (v : ℝ → Homogenization.Vec 2 → ℝ) {r : ℝ} (hr : s / 2 < r) : advDiffOp b κ (cutoffV s v) r = advDiffOp b κ v r

theorem AVenhance.Infra.Section5.Integration.EnergyIoi.errGrad_cutoffV (u : ℝ → Homogenization.Vec 2 → ℝ) {s : ℝ} (hs : 0 < s) (v : ℝ → Homogenization.Vec 2 → ℝ) {r : ℝ} (hr : s / 2 ≤ r) : Energy.errGrad u (cutoffV s v) r = Energy.errGrad u v r

The slice gradient energy of the cut-off function agrees with that of v for t ≥ s/2.

theorem AVenhance.Infra.Section5.Integration.EnergyIoi.IoiSetup.forcing_continuousOn {φ : ℝ → Homogenization.Vec 2 → ℝ} {κ : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {u v : ℝ → Homogenization.Vec 2 → ℝ} (S : IoiSetup φ κ θ₀ u v) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => advDiffOp (streamVel φ) κ v p.1 p.2) Classical.classicalPositiveTimeDomain

The defect of v is jointly continuous on (0,∞) × ℝ².