SourceErrorDContract: the contract norm versus the space-time L² norm

The contract states d_m as the time-L² of the spatial L² norm (gradNormSq). For a field measurable on the time cube this is at most 2 ‖d_m‖_{L²((0,1)×𝕋²)} (sup norm on Vec 2, Tonelli).

theorem AVenhance.Infra.Section5.Contracts.sed_vecNormSq_le (v : Homogenization.Vec 2) : Homogenization.vecNormSq v ≤ 2 * ‖v‖ ^ 2

theorem AVenhance.Infra.Section5.Contracts.sed_ofReal_gradNormSq_le (u : Homogenization.Vec 2 → Homogenization.Vec 2) : ENNReal.ofReal √(gradNormSq u) ^ 2 ≤ 2 * ∫⁻ (x : Homogenization.Vec 2) in unitCube, ‖u x‖ₑ ^ 2

theorem AVenhance.Infra.Section5.Contracts.sed_lhs_le_eLpNorm (d : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hd : MeasureTheory.AEStronglyMeasurable (fun (z : ℝ × Homogenization.Vec 2) => d z.1 z.2) (MeasureTheory.volume.restrict timeCube)) : (∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal √(gradNormSq (d t)) ^ 2) ^ (1 / 2) ≤ 2 * MeasureTheory.eLpNorm (fun (z : ℝ × Homogenization.Vec 2) => d z.1 z.2) 2 (MeasureTheory.volume.restrict timeCube)