Time-integral Cauchy bounds used for the regular and flux pairings in the transported H_m estimate.

theorem AVenhance.Infra.Section4.hm_interval_integral_abs_le_sqrt_length_mul_l2 {a b Q : ℝ} {f : ℝ → ℝ} (hab : a ≤ b) (hQ : 0 ≤ Q) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) (hfSq : ∫ (t : ℝ) in Set.Ioc a b, f t ^ 2 ≤ Q ^ 2) : |∫ (t : ℝ) in a..b, f t| ≤ √(b - a) * Q

Scalar Cauchy--Schwarz on a finite time interval, with the exact interval length factor retained.

theorem AVenhance.Infra.Section4.hm_interval_integral_product_abs_le_l2 {a b A B : ℝ} {f g : ℝ → ℝ} (hab : a ≤ b) (hA : 0 ≤ A) (hB : 0 ≤ B) (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) (hfSq : ∫ (t : ℝ) in Set.Ioc a b, f t ^ 2 ≤ A ^ 2) (hgSq : ∫ (t : ℝ) in Set.Ioc a b, g t ^ 2 ≤ B ^ 2) : |∫ (t : ℝ) in a..b, f t * g t| ≤ A * B

Cauchy--Schwarz for a product over an interval, with each L² energy bounded separately.

theorem AVenhance.Infra.Section4.hm_unitCube_scalar_pairing_abs_le {f g : Homogenization.Vec 2 → ℝ} (hf : Continuous f) (hg : Continuous g) : |∫ (x : Homogenization.Vec 2) in unitCube, f x * g x| ≤ √(l2NormSq f) * √(l2NormSq g)

Spatial Cauchy--Schwarz for the regular source pairing on the torus cell.

theorem AVenhance.Infra.Section4.HmPairingEstimates.hm_vecNormSq_nonneg (u : Homogenization.Vec 2) : 0 ≤ Homogenization.vecNormSq u

theorem AVenhance.Infra.Section4.HmPairingEstimates.hm_vecDot_abs_le_norm (u v : Homogenization.Vec 2) : |Homogenization.vecDot u v| ≤ √(Homogenization.vecNormSq u) * √(Homogenization.vecNormSq v)

theorem AVenhance.Infra.Section4.hm_unitCube_vector_pairing_abs_le {F V : Homogenization.Vec 2 → Homogenization.Vec 2} (hF : Continuous F) (hV : Continuous V) : |∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (F x) (V x)| ≤ √(gradNormSq F) * √(gradNormSq V)

Spatial Cauchy--Schwarz for a vector flux pairing on the torus cell.

theorem AVenhance.Infra.Section4.hm_regular_pairing_interval_bound_of_l2 {F G : ℝ → Homogenization.Vec 2 → ℝ} {a b H Q : ℝ} (hab : a ≤ b) (hH : 0 ≤ H) (hQ : 0 ≤ Q) (hFbound : ∀ s ∈ Set.Ioc a b, √(l2NormSq (F s)) ≤ H) (hFcont : ∀ s ∈ Set.Ioc a b, Continuous (F s)) (hGcont : ∀ s ∈ Set.Ioc a b, Continuous (G s)) (hGnorm : MeasureTheory.MemLp (fun (s : ℝ) => √(l2NormSq (G s))) 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) (hGsq : ∫ (s : ℝ) in Set.Ioc a b, √(l2NormSq (G s)) ^ 2 ≤ Q ^ 2) (hGint : MeasureTheory.Integrable (fun (s : ℝ) => √(l2NormSq (G s))) (MeasureTheory.volume.restrict (Set.Ioc a b))) (hPairAbsInt : MeasureTheory.Integrable (fun (s : ℝ) => |hmRegularPairing s|) (MeasureTheory.volume.restrict (Set.Ioc a b))) : |∫ (s : ℝ) in a..b, hmRegularPairing s| ≤ √(b - a) * Q * H

The integrated regular pairing is bounded using only an envelope for F and the time L² energy of G.

theorem AVenhance.Infra.Section4.hm_flux_pairing_interval_bound_of_l2 {F : ℝ → Homogenization.Vec 2 → ℝ} {V : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {a b QF QV : ℝ} (hab : a ≤ b) (hQF : 0 ≤ QF) (hQV : 0 ≤ QV) (hGradCont : ∀ s ∈ Set.Ioc a b, Continuous (spaceGrad (F s))) (hVcont : ∀ s ∈ Set.Ioc a b, Continuous (V s)) (hFnorm : MeasureTheory.MemLp (fun (s : ℝ) => √(gradNormSq fun (x : Homogenization.Vec 2) => spaceGrad (F s) x)) 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) (hVnorm : MeasureTheory.MemLp (fun (s : ℝ) => √(gradNormSq (V s))) 2 (MeasureTheory.volume.restrict (Set.Ioc a b))) (hFsq : ∫ (s : ℝ) in Set.Ioc a b, √(gradNormSq fun (x : Homogenization.Vec 2) => spaceGrad (F s) x) ^ 2 ≤ QF ^ 2) (hVsq : ∫ (s : ℝ) in Set.Ioc a b, √(gradNormSq (V s)) ^ 2 ≤ QV ^ 2) (hPairAbsInt : MeasureTheory.Integrable (fun (s : ℝ) => |hmFluxPairing s|) (MeasureTheory.volume.restrict (Set.Ioc a b))) : |∫ (s : ℝ) in a..b, hmFluxPairing s| ≤ QF * QV

The integrated gradient--flux pairing is controlled by the product of the time L² norms of the two spatial vector fields.