L² estimates on the closed time-space cell used by the differentiated energy recursion.

def AVenhance.Infra.Section4.ThetaSpaceTime.thetaTimeClosedCell : Set (ℝ × Homogenization.Vec 2)

Closed time-space unit cell for the temperature space-time estimates.

Equations

• AVenhance.Infra.Section4.ThetaSpaceTime.thetaTimeClosedCell = Set.Icc 0 1 ×ˢ Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Section4.ThetaSpaceTime.thetaTimeClosedCell_compact : IsCompact thetaTimeClosedCell

theorem AVenhance.Infra.Section4.ThetaSpaceTime.thetaTimeCube_subset_closedCell : timeCube ⊆ thetaTimeClosedCell

theorem AVenhance.Infra.Section4.theta_continuous_timeCube_memLp_two {f : ℝ × Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.MemLp f (ENNReal.ofReal 2) (MeasureTheory.volume.restrict timeCube)

Every continuous function is square-integrable on the space-time cell. The compact closed cell gives both finite measure and a uniform bound.

theorem AVenhance.Infra.Section4.theta_timeCube_integral_mul_abs_le {f g : ℝ × Homogenization.Vec 2 → ℝ} (hf : Continuous f) (hg : Continuous g) : |∫ (p : ℝ × Homogenization.Vec 2) in timeCube, f p * g p| ≤ √(∫ (p : ℝ × Homogenization.Vec 2) in timeCube, f p ^ 2) * √(∫ (p : ℝ × Homogenization.Vec 2) in timeCube, g p ^ 2)

Cauchy–Schwarz for products integrated over the full space-time cell.

theorem AVenhance.Infra.Section4.theta_timeCube_integral_eq_interval_integral {f : ℝ × Homogenization.Vec 2 → ℝ} (hf : Continuous f) : ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, f p = ∫ (t : ℝ) in 0..1, ∫ (x : Homogenization.Vec 2) in unitCube, f (t, x)

Fubini on the open time-space cell, with the time integral written in the paper's interval convention. The omitted right endpoint is null.

theorem AVenhance.Infra.Section4.theta_timeCube_integral_mul_bounded_le {f g a : ℝ × Homogenization.Vec 2 → ℝ} {M : ℝ} (hf : Continuous f) (hg : Continuous g) (ha : Continuous a) (hM : 0 ≤ M) (haM : ∀ p ∈ timeCube, |a p| ≤ M) : |∫ (p : ℝ × Homogenization.Vec 2) in timeCube, f p * (a p * g p)| ≤ M * √(∫ (p : ℝ × Homogenization.Vec 2) in timeCube, f p ^ 2) * √(∫ (p : ℝ × Homogenization.Vec 2) in timeCube, g p ^ 2)

Cauchy--Schwarz with a bounded coefficient on the space-time cell.