SourceErrorDContract: open-time regularity and measurability inputs

The iterates T_i are smooth only for t ≥ 0, so the global continuity of ∇T in the dm_pulled_gradient_* lemmas is replaced by continuity on Ici 0 ×ˢ univ through the time clamp sedClamp, which changes nothing on the open time cube.

theorem AVenhance.Infra.Section5.Contracts.sed_gradient_continuousOn {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {F u : ℝ → Homogenization.Vec 2 → ℝ} {u₀ : Homogenization.Vec 2 → ℝ} (hu : IsClassicalSol b κ F u₀ u) : ContinuousOn (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (u z.1) z.2) (Set.Ici 0 ×ˢ Set.univ)

A classical solution has continuous spatial gradient on Ici 0 ×ˢ univ.

def AVenhance.Infra.Section5.Contracts.sedClamp (T : ℝ → Homogenization.Vec 2 → ℝ) : ℝ → Homogenization.Vec 2 → ℝ

The time-clamped copy of T: it agrees with T on t ≥ 0 and has globally continuous spatial gradient.

Equations

• AVenhance.Infra.Section5.Contracts.sedClamp T t = T (max t 0)

theorem AVenhance.Infra.Section5.Contracts.sedClamp_gradient_continuous {T : ℝ → Homogenization.Vec 2 → ℝ} (hc : ContinuousOn (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (T z.1) z.2) (Set.Ici 0 ×ˢ Set.univ)) : Continuous fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (sedClamp T z.1) z.2

theorem AVenhance.Infra.Section5.Contracts.sedClamp_grad_eq {T : ℝ → Homogenization.Vec 2 → ℝ} {z : ℝ × Homogenization.Vec 2} (hz : 0 ≤ z.1) : spaceGrad (sedClamp T z.1) z.2 = spaceGrad (T z.1) z.2

theorem AVenhance.Infra.Section5.Contracts.sedClamp_energy_eq (T : ℝ → Homogenization.Vec 2 → ℝ) : (spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (sedClamp T t)) = spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (T t)

theorem AVenhance.Infra.Section5.Contracts.sed_timeCube_ae_nonneg : ∀ᵐ (z : ℝ × Homogenization.Vec 2) ∂MeasureTheory.volume.restrict timeCube, 0 ≤ z.1

theorem AVenhance.Infra.Section5.Contracts.dmFrozenFluxFirst_eq_hmFrozenDFirstFlux {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) : Section4.dmFrozenFluxFirst I hΦ m κ T = fun (z : ℝ × Homogenization.Vec 2) => Section4.hmFrozenDFirstFlux I hΦ m κ T z.1 z.2

The Section 4 d_m first summand is the first summand hmFrozenDFirstFlux.

theorem AVenhance.Infra.Section5.Contracts.sed_Tgrad_eLpNorm_le {T : ℝ → Homogenization.Vec 2 → ℝ} (hc : ContinuousOn (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (T z.1) z.2) (Set.Ici 0 ×ˢ Set.univ)) {κprev N : ℝ} (hκprev : 0 < κprev) (hT : √κprev * √(spaceTimeGradNormSq fun (t : ℝ) => spaceGrad (T t)) ≤ N) : MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (T z.1) z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal (N / √κprev)

The temperature-gradient L² bound for the actual (open-time smooth) T, from the profile, through the time clamp.

theorem AVenhance.Infra.Section5.Contracts.sed_measurable_mulVec {α : Type u_1} [MeasurableSpace α] {A : α → Matrix (Fin 2) (Fin 2) ℝ} {v : α → Homogenization.Vec 2} (hA : ∀ (i j : Fin 2), Measurable fun (a : α) => A a i j) (hv : Measurable v) : Measurable fun (a : α) => (A a).mulVec (v a)

The matrix-vector product of measurable entries is measurable.

theorem AVenhance.Infra.Section5.Contracts.sed_firstMeas {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κ : ℝ} (hκ : 0 < κ) {T : ℝ → Homogenization.Vec 2 → ℝ} (hc : ContinuousOn (fun (z : ℝ × Homogenization.Vec 2) => spaceGrad (T z.1) z.2) (Set.Ici 0 ×ˢ Set.univ)) : MeasureTheory.AEStronglyMeasurable (Section4.dmFrozenFluxFirst I hΦ m κ T) (MeasureTheory.volume.restrict timeCube)

Measurability of the first term of d_m.

theorem AVenhance.Infra.Section5.Contracts.sed_amnrEntry_meas {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm κprev : ℝ} (hκm : 0 < κm) {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hθprev : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (n : ℕ) (i j k : Fin 2) : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => I.Amnr hΦ m κm n (T (Nstar β)) (Jcut β) z.1 z.2 i j k) (MeasureTheory.volume.restrict timeCube)

The terminal AMNR tensor entries are measurable on the time cube.

theorem AVenhance.Infra.Section5.Contracts.sed_coordinate_meas {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (n : ℕ) (i j k : Fin 2) (hA : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => I.Amnr hΦ m κ n T (Jcut β) z.1 z.2 i j k) (MeasureTheory.volume.restrict timeCube)) : MeasureTheory.AEStronglyMeasurable (Section4.dmFrozenTailCoordinateTerm I hΦ m κ T n i j k) (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.Section5.Contracts.sed_sourceErrorD_meas {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κ : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (hfirst : MeasureTheory.AEStronglyMeasurable (Section4.dmFrozenFluxFirst I hΦ m κ T) (MeasureTheory.volume.restrict timeCube)) (hcoord : ∀ n ∈ Finset.range (Nstar β), ∀ (i j k : Fin 2), MeasureTheory.AEStronglyMeasurable (Section4.dmFrozenTailCoordinateTerm I hΦ m κ T n i j k) (MeasureTheory.volume.restrict timeCube)) : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => sourceErrorD I hΦ m κ T z.1 z.2) (MeasureTheory.volume.restrict timeCube)

The whole d_m field is measurable on the time cube.