LeanPool.AnomalousDiffusion.AVenhance.Infra.Section4.HmPairingPrefix

Full-cell time-L² data restrict to every prefix, so the scalar and flux pairing Cauchy estimates can be applied uniformly to moving half-cell base points.

theorem AVenhance.Infra.Section4.hm_time_l2_data_restrict {g : ℝ → ℝ} {A B a b Q : ℝ} (hAa : A ≤ a) (hbB : b ≤ B) (hNorm : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Set.Ioc A B))) (hSq : ∫ (t : ℝ) in Set.Ioc A B, g t ^ 2 ≤ Q ^ 2) (hInt : MeasureTheory.Integrable g (MeasureTheory.volume.restrict (Set.Ioc A B))) :

MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (Set.Ioc a b)) ∧ ∫ (t : ℝ) in Set.Ioc a b, g t ^ 2 ≤ Q ^ 2 ∧ MeasureTheory.Integrable g (MeasureTheory.volume.restrict (Set.Ioc a b))

Restrict an L² time-slice datum from the whole positive-time interval to a smaller closed cell, retaining both its norm and integrability bounds.

source

theorem AVenhance.Infra.Section4.hm_time_slice_l2_data_of_spatial_energy {G : ℝ → Homogenization.Vec 2 → ℝ} {a b Q : ℝ} (hMeas : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => √(l2NormSq (G t))) (MeasureTheory.volume.restrict (Set.Ioc a b))) (hEnergyInt : MeasureTheory.Integrable (fun (t : ℝ) => l2NormSq (G t)) (MeasureTheory.volume.restrict (Set.Ioc a b))) (hEnergy : ∫ (t : ℝ) in Set.Ioc a b, l2NormSq (G t) ≤ Q ^ 2) :

MeasureTheory.MemLp (fun (t : ℝ) => √(l2NormSq (G t))) 2 (MeasureTheory.volume.restrict (Set.Ioc a b)) ∧ ∫ (t : ℝ) in Set.Ioc a b, √(l2NormSq (G t)) ^ 2 ≤ Q ^ 2 ∧ MeasureTheory.Integrable (fun (t : ℝ) => √(l2NormSq (G t))) (MeasureTheory.volume.restrict (Set.Ioc a b))

Convert an integrable spatial energy function into the time-L² datum of its spatial norm. The separate measurability hypothesis is the Fubini interface for the slice norm.

source

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

|∫ (r : ℝ) in c..s, hmRegularPairing r| ≤ √|s - c| * Q * H

Cauchy--Schwarz for a prefix measured from any base point in a full cell. The interval orientation is immaterial, and the exact distance from the base point is retained.

source

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

|∫ (r : ℝ) in c..s, hmFluxPairing r| ≤ QF * QV

Flux-pairing Cauchy--Schwarz on a subinterval of a full cell, with an arbitrary base point and either orientation.