The homogeneous negative Sobolev duality on the unit torus

noncomputable def AVenhance.Infra.Ergodic.gradientL2SquaredAverage {d : ℕ} (φ : Homogenization.Vec d → ℝ) : ℝ

The squared L² norm of the coordinate gradient on the unit cell.

Equations

• AVenhance.Infra.Ergodic.gradientL2SquaredAverage φ = AVenhance.Infra.Ergodic.cellAverage fun (x : Homogenization.Vec d) => ∑ i : Fin d, (fderiv ℝ φ x) (Pi.single i 1) ^ 2

def AVenhance.Infra.Ergodic.HMinusOneTest (d : ℕ) : Type

Smooth periodic mean-zero representatives with gradient norm at most one, used for the homogeneous dual test space.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AVenhance.Infra.Ergodic.homogeneousHMinusOneNorm {d : ℕ} (h : Homogenization.Vec d → ℝ) : ENNReal

The homogeneous H⁻¹ dual seminorm, represented as an extended nonnegative real to allow the defining supremum before its finiteness is proved.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Ergodic.HMinusOne.unitCellSet_eq_torusUnitCell (d : ℕ) : unitCellSet d = Torus.unitCell d

def AVenhance.Infra.Ergodic.HMinusOne.closedUnitCube (d : ℕ) : Set (Homogenization.Vec d)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Ergodic.HMinusOne.closedUnitCube d = Set.univ.pi fun (x : Fin d) => Set.Icc 0 1

theorem AVenhance.Infra.Ergodic.HMinusOne.unitCell_subset_closedUnitCube (d : ℕ) : Torus.unitCell d ⊆ closedUnitCube d

theorem AVenhance.Infra.Ergodic.HMinusOne.continuousComplex_unitCell_integrable {d : ℕ} {u : Homogenization.Vec d → ℂ} (hu : Continuous u) : MeasureTheory.IntegrableOn u (Torus.unitCell d) MeasureTheory.volume

theorem AVenhance.Infra.Ergodic.dualPairing_le_homogeneousHMinusOneNorm {d : ℕ} (h : Homogenization.Vec d → ℝ) (φ : HMinusOneTest d) : ENNReal.ofReal |cellAverage fun (x : Homogenization.Vec d) => h x * ↑φ x| ≤ homogeneousHMinusOneNorm h

Every admissible dual pairing is bounded by the homogeneous H⁻¹ seminorm.

theorem AVenhance.Infra.Ergodic.HMinusOne.coordDeriv_realCast {d : ℕ} {f : Homogenization.Vec d → ℝ} (hf : ContDiff ℝ 1 f) (i : Fin d) (x : Homogenization.Vec d) : Torus.coordDeriv i (fun (y : Homogenization.Vec d) => ↑(f y)) x = ↑((fderiv ℝ f x) (Homogenization.basisVec i))

theorem AVenhance.Infra.Ergodic.homogeneousHMinusOneNorm_le_of_cellL2 {d : ℕ} (hd : 0 < d) {h : Homogenization.Vec d → ℝ} (hL2 : MeasureTheory.MemLp h (ENNReal.ofReal 2) (MeasureTheory.volume.restrict (Torus.unitCell d))) : homogeneousHMinusOneNorm h ≤ ENNReal.ofReal ((∫ (x : Homogenization.Vec d) in Torus.unitCell d, h x ^ 2) ^ (1 / 2) * (4 * Real.pi ^ 2)⁻¹ ^ (1 / 2))

A Poincaré dual bound for the homogeneous H⁻¹ seminorm. This is the basic dual step used after an independent estimate of the product's cell L² norm.

Divergence certificates

The source proof's frequency split is intended to produce a small vector potential for its low-frequency product. This duality lemma records the analytic estimate needed after that construction: a periodic divergence has homogeneous H⁻¹ norm bounded by the L² norm of its potential.

noncomputable def AVenhance.Infra.Ergodic.vectorFieldL2SquaredAverage {d : ℕ} (V : Fin d → Homogenization.Vec d → ℝ) : ℝ

The cell-averaged squared size of a real vector field.

Equations

• AVenhance.Infra.Ergodic.vectorFieldL2SquaredAverage V = AVenhance.Infra.Ergodic.cellAverage fun (x : Homogenization.Vec d) => ∑ i : Fin d, V i x ^ 2

theorem AVenhance.Infra.Ergodic.HMinusOne.cellAverage_const_mul {d : ℕ} (c : ℝ) (f : Homogenization.Vec d → ℝ) : (cellAverage fun (x : Homogenization.Vec d) => c * f x) = c * cellAverage f

theorem AVenhance.Infra.Ergodic.homogeneousHMinusOneNorm_flow_le_of_testComposition {d : ℕ} {f g : Homogenization.Vec d → ℝ} (hf : IsZPeriodic f) (hg : IsZPeriodic g) (X : PeriodicVolumePreservingDiffeomorphism d) (L : ℝ) (hL : 0 < L) (hmap : ∀ (φ : Homogenization.Vec d → ℝ), ContDiff ℝ (↑⊤) φ → IsZPeriodic φ → cellAverage φ = 0 → gradientL2SquaredAverage φ ≤ 1 → (gradientL2SquaredAverage fun (x : Homogenization.Vec d) => L⁻¹ * φ (X.toFun x)) ≤ 1) : (homogeneousHMinusOneNorm fun (x : Homogenization.Vec d) => f x * g (X.invFun x)) ≤ ENNReal.ofReal L * homogeneousHMinusOneNorm fun (x : Homogenization.Vec d) => f (X.toFun x) * g x

Flow transport for the homogeneous dual norm. The hmap premise states the precise test-function bound needed after composing tests with X and rescaling them into the unit gradient ball. A derivative bound on X implies this premise through the chain rule and measure preservation.