Fubini converts a spacetime scalar L² bound into the time-L² datum of the spatial slice norm used by the pairing prefix estimates.
theorem
AVenhance.Infra.Section4.hm_time_slice_l2_data_of_spacetime_square
{G : ℝ → Homogenization.Vec 2 → ℝ}
{Q : ℝ}
(hGsqInt :
MeasureTheory.Integrable (fun (z : ℝ × Homogenization.Vec 2) => G z.1 z.2 ^ 2)
(MeasureTheory.volume.restrict timeCube))
(hGsqBound : ∫ (z : ℝ × Homogenization.Vec 2) in timeCube, G z.1 z.2 ^ 2 ≤ Q ^ 2)
:
On the open time-space cell, the spacetime square integral is the time
integral of the spatial L² energy. Consequently its bound supplies the
time-L² data for the prefix Cauchy estimates.
theorem
AVenhance.Infra.Section4.hm_time_slice_l2_data_of_spacetime_eLpNorm
{G : ℝ → Homogenization.Vec 2 → ℝ}
{Q : ℝ}
(hGmeas :
MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => G z.1 z.2)
(MeasureTheory.volume.restrict timeCube))
(hQ : 0 ≤ Q)
(hGbound :
MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => G z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal Q)
:
A spacetime scalar eLpNorm estimate supplies the full time-slice
L² datum, with the same amplitude. Measurability is the only separate
input; in the source it follows from the coefficient and gradient
entry measurability.
theorem
AVenhance.Infra.Section4.hm_vector_time_slice_l2_data_of_spacetime_eLpNorm
{V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2}
{Q : ℝ}
(hVmeas :
MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => V z.1 z.2)
(MeasureTheory.volume.restrict timeCube))
(hVmagMeas :
MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => √(Homogenization.vecNormSq (V z.1 z.2)))
(MeasureTheory.volume.restrict timeCube))
(hQ : 0 ≤ Q)
(hVbound :
MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => V z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube) ≤ ENNReal.ofReal Q)
:
MeasureTheory.MemLp (fun (t : ℝ) => √(gradNormSq (V t))) 2 (MeasureTheory.volume.restrict (Set.Ioc 0 1)) ∧ ∫ (t : ℝ) in Set.Ioc 0 1, √(gradNormSq (V t)) ^ 2 ≤ (√2 * Q) ^ 2 ∧ MeasureTheory.Integrable (fun (t : ℝ) => √(gradNormSq (V t))) (MeasureTheory.volume.restrict (Set.Ioc 0 1))
A vector-valued spacetime L² bound gives time-slice data for its
Euclidean spatial energy. Vec 2 carries the Pi sup norm in eLpNorm, so
the conversion to vecNormSq costs the explicit factor √2.