Consequences of timeHMinusOneNorm f ≠ ⊤

With measurability of t ↦ ‖f t‖_{HDot⁻¹} on (0,1), finiteness of the time norm gives: the norm is finite for a.e. t ∈ (0,1), its square is integrable, and the real square of (timeHMinusOneNorm f).toReal is the integral of the squares.

theorem AVenhance.Infra.Section5.Integration.Energy.FiniteNorm.lintegral_ne_top_of_timeNorm {f : ℝ → Homogenization.Vec 2 → ℝ} (hfin : timeHMinusOneNorm f ≠ ⊤) : ∫⁻ (t : ℝ) in Set.Ioo 0 1, hMinusOneNorm (f t) ^ 2 ≠ ⊤

theorem AVenhance.Infra.Section5.Integration.Energy.FiniteNorm.aemeasurable_sq {f : ℝ → Homogenization.Vec 2 → ℝ} (hm : AEMeasurable (fun (t : ℝ) => hMinusOneNorm (f t)) (MeasureTheory.volume.restrict (Set.Ioo 0 1))) : AEMeasurable (fun (t : ℝ) => hMinusOneNorm (f t) ^ 2) (MeasureTheory.volume.restrict (Set.Ioo 0 1))

theorem AVenhance.Infra.Section5.Integration.Energy.ae_hMinusOneNorm_ne_top {f : ℝ → Homogenization.Vec 2 → ℝ} (hm : AEMeasurable (fun (t : ℝ) => hMinusOneNorm (f t)) (MeasureTheory.volume.restrict (Set.Ioo 0 1))) (hfin : timeHMinusOneNorm f ≠ ⊤) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 1), hMinusOneNorm (f t) ≠ ⊤

Almost every slice has finite HDot⁻¹ norm.

theorem AVenhance.Infra.Section5.Integration.Energy.integrable_toReal_sq {f : ℝ → Homogenization.Vec 2 → ℝ} (hm : AEMeasurable (fun (t : ℝ) => hMinusOneNorm (f t)) (MeasureTheory.volume.restrict (Set.Ioo 0 1))) (hfin : timeHMinusOneNorm f ≠ ⊤) : MeasureTheory.Integrable (fun (t : ℝ) => (hMinusOneNorm (f t)).toReal ^ 2) (MeasureTheory.volume.restrict (Set.Ioo 0 1))

The squared real norms are integrable on (0,1).

theorem AVenhance.Infra.Section5.Integration.Energy.integral_toReal_sq_eq {f : ℝ → Homogenization.Vec 2 → ℝ} (hm : AEMeasurable (fun (t : ℝ) => hMinusOneNorm (f t)) (MeasureTheory.volume.restrict (Set.Ioo 0 1))) (hfin : timeHMinusOneNorm f ≠ ⊤) : (timeHMinusOneNorm f).toReal ^ 2 = ∫ (t : ℝ) in Set.Ioo 0 1, (hMinusOneNorm (f t)).toReal ^ 2

(timeHMinusOneNorm f).toReal ^ 2 is the integral of the squared real norms.