Tools for the extended-valued homogeneous negative norm. The mean-zero bridge retains the distinction between all periodic tests and the centred tests used in Ergodic.

theorem AVenhance.Infra.Section5.avInfraSection5HMinusToolsIsFiniteMeasure1 : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.Section5.HMinusTools.cell_average_frozen (f : Homogenization.Vec 2 → ℝ) : Ergodic.cellAverage f = ∫ (x : Homogenization.Vec 2) in unitCube, f x

theorem AVenhance.Infra.Section5.HMinusTools.continuous_memL2 {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.Section5.HMinusTools.gradient_average (φ : Homogenization.Vec 2 → ℝ) : Ergodic.gradientL2SquaredAverage φ = gradNormSq (spaceGrad φ)

theorem AVenhance.Infra.Section5.HMinusTools.pair_integrable {g φ : Homogenization.Vec 2 → ℝ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict unitCube)) (hφ : Continuous φ) : MeasureTheory.IntegrableOn (fun (x : Homogenization.Vec 2) => g x * φ x) unitCube MeasureTheory.volume

theorem AVenhance.Infra.Section5.ergodic_hMinusOneNorm_le_frozen (g : Homogenization.Vec 2 → ℝ) : Ergodic.homogeneousHMinusOneNorm g ≤ hMinusOneNorm g

The App C analytic, centred test norm is bounded by the smooth-test norm. The reverse inequality would need a density argument; it is not assumed.

theorem AVenhance.Infra.Section5.hMinusOneNorm_le_L2 {g : Homogenization.Vec 2 → ℝ} (hg : Homogenization.MemL2On unitCube g) (hm : Homogenization.MeanZeroOn unitCube g) : hMinusOneNorm g ≤ ENNReal.ofReal ((2 * Real.pi)⁻¹ * √(l2NormSq g))

Poincare duality in the carriers, with its sharp torus constant.

theorem AVenhance.Infra.Section5.hMinusOneNorm_le_of_divergence {h : Homogenization.Vec 2 → ℝ} {V : Fin 2 → Homogenization.Vec 2 → ℝ} (hVdiff : ∀ (i : Fin 2), ContDiff ℝ (↑⊤) (V i)) (hVper : ∀ (i : Fin 2), Ergodic.IsZPeriodic (V i)) (hdiv : ∀ (x : Homogenization.Vec 2), h x = ∑ i : Fin 2, (fderiv ℝ (V i) x) (Homogenization.basisVec i)) : hMinusOneNorm h ≤ ENNReal.ofReal √(Ergodic.vectorFieldL2SquaredAverage V)

Divergence duality for the C-infinity test class. This transfers the integration-by-parts proof underlying the analytic-test estimate, rather than asserting an unproved equality of the two test suprema.

noncomputable def AVenhance.Infra.Section5.cellDivergence (F : Homogenization.Vec 2 → Homogenization.Vec 2) (x : Homogenization.Vec 2) : ℝ

Classical divergence written coordinatewise on the Vec carrier.

Equations

• AVenhance.Infra.Section5.cellDivergence F x = ∑ i : Fin 2, (fderiv ℝ (fun (y : Homogenization.Vec 2) => F y i) x) (Homogenization.basisVec i)

theorem AVenhance.Infra.Section5.hMinusOneNorm_divergence_le (F : Homogenization.Vec 2 → Homogenization.Vec 2) (hF : ContDiff ℝ (↑⊤) F) (hp : IsZ2Periodic F) : hMinusOneNorm (cellDivergence F) ≤ ENNReal.ofReal √(gradNormSq F)

Vector-field form of divergence duality, with the Euclidean energy.

theorem AVenhance.Infra.Section5.hMinusOneNorm_add_le {f g : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) (hg : Homogenization.MemL2On unitCube g) : (hMinusOneNorm fun (x : Homogenization.Vec 2) => f x + g x) ≤ hMinusOneNorm f + hMinusOneNorm g

Triangle inequality; L2 hypotheses justify addition of the dual integrals. Means need not vanish: the extended norm retains infinite values.

theorem AVenhance.Infra.Section5.hMinusOneNorm_const_mul (a : ℝ) (g : Homogenization.Vec 2 → ℝ) : (hMinusOneNorm fun (x : Homogenization.Vec 2) => a * g x) = ENNReal.ofReal |a| * hMinusOneNorm g

Exact scaling, valid even for infinite negative norm.

noncomputable def AVenhance.Infra.Section5.timeHMinusOneNorm (f : ℝ → Homogenization.Vec 2 → ℝ) : ENNReal

Exactly the time-norm carrier occurring in the BigBound statement.

Equations

• AVenhance.Infra.Section5.timeHMinusOneNorm f = (∫⁻ (t : ℝ) in Set.Ioo 0 1, AVenhance.hMinusOneNorm (f t) ^ 2) ^ (1 / 2)

theorem AVenhance.Infra.Section5.timeHMinusOneNorm_add_le {f g : ℝ → Homogenization.Vec 2 → ℝ} (hf : ∀ t ∈ Set.Ioo 0 1, Homogenization.MemL2On unitCube (f t)) (hg : ∀ t ∈ Set.Ioo 0 1, Homogenization.MemL2On unitCube (g t)) (hmf : AEMeasurable (fun (t : ℝ) => hMinusOneNorm (f t)) (MeasureTheory.volume.restrict (Set.Ioo 0 1))) (hmg : AEMeasurable (fun (t : ℝ) => hMinusOneNorm (g t)) (MeasureTheory.volume.restrict (Set.Ioo 0 1))) : (timeHMinusOneNorm fun (t : ℝ) (x : Homogenization.Vec 2) => f t x + g t x) ≤ timeHMinusOneNorm f + timeHMinusOneNorm g

Time-integrated Minkowski, with explicit measurability of the two norms.

theorem AVenhance.Infra.Section5.timeHMinusOneNorm_le_of_bound {f : ℝ → Homogenization.Vec 2 → ℝ} {B : ℝ → ENNReal} (h : ∀ t ∈ Set.Ioo 0 1, hMinusOneNorm (f t) ≤ B t) : timeHMinusOneNorm f ≤ (∫⁻ (t : ℝ) in Set.Ioo 0 1, B t ^ 2) ^ (1 / 2)

Pointwise bounds pass to the exact BigBound time norm.

theorem AVenhance.Infra.Section5.timeHMinusOneNorm_le_L2 {f : ℝ → Homogenization.Vec 2 → ℝ} (hf : ∀ t ∈ Set.Ioo 0 1, Homogenization.MemL2On unitCube (f t)) (hm : ∀ t ∈ Set.Ioo 0 1, Homogenization.MeanZeroOn unitCube (f t)) : timeHMinusOneNorm f ≤ (∫⁻ (t : ℝ) in Set.Ioo 0 1, ENNReal.ofReal ((2 * Real.pi)⁻¹ * √(l2NormSq (f t))) ^ 2) ^ (1 / 2)

Time-integrated L2-to-negative-norm estimate in carriers.

noncomputable def AVenhance.Infra.Section5.periodicPrimitive (g : ℝ → ℝ) (t : ℝ) : ℝ

The time primitive based at 0, without a mean correction.

Equations

• AVenhance.Infra.Section5.periodicPrimitive g t = ∫ (s : ℝ) in 0..t, g s

theorem AVenhance.Infra.Section5.periodicPrimitive_hasDerivAt {g : ℝ → ℝ} (hg : Continuous g) (t : ℝ) : HasDerivAt (periodicPrimitive g) (g t) t

The primitive is an actual antiderivative, not only a periodic integral.

theorem AVenhance.Infra.Section5.periodicPrimitive_periodic {g : ℝ → ℝ} {T : ℝ} (hg : Continuous g) (hp : Function.Periodic g T) (hm : ∫ (s : ℝ) in 0..T, g s = 0) : Function.Periodic (periodicPrimitive g) T

A mean-zero period integral makes the primitive periodic.

theorem AVenhance.Infra.Section5.periodicPrimitive_abs_le {g : ℝ → ℝ} {T B : ℝ} (hT : 0 < T) (hg : Continuous g) (hp : Function.Periodic g T) (hm : ∫ (s : ℝ) in 0..T, g s = 0) (hB : 0 ≤ B) (hb : ∀ t ∈ Set.Icc 0 T, |g t| ≤ B) (t : ℝ) : |periodicPrimitive g t| ≤ T * B

Global supremum bound in a pointwise form, retaining all real times. A bound just on one period is sufficient by periodicity.