Exact averages of the integer-frequency trigonometric modes in §3.

theorem AVenhance.Infra.Section3.SpaceAverages.sin_square_periodic_one : Function.Periodic (fun (x : ℝ) => Real.sin (2 * Real.pi * x) ^ 2) 1

theorem AVenhance.Infra.Section3.SpaceAverages.sin_periodic_one : Function.Periodic (fun (x : ℝ) => Real.sin (2 * Real.pi * x)) 1

theorem AVenhance.Infra.Section3.intervalAverage_sin_square_nat (n : ℕ) (hn : 0 < n) : ∫ (x : ℝ) in 0..1, Real.sin (2 * Real.pi * ↑n * x) ^ 2 = 1 / 2

The square of an integer-frequency sine has unit-cell mean 1/2.

theorem AVenhance.Infra.Section3.intervalAverage_sin_nat (n : ℕ) : ∫ (x : ℝ) in 0..1, Real.sin (2 * Real.pi * ↑n * x) = 0

An integer-frequency sine has zero unit-cell mean.

def AVenhance.Infra.Section3.SpaceAverages.closedUnitSquare : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Section3.SpaceAverages.closedUnitSquare = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Section3.SpaceAverages.continuous_coord_integrableOn_unitCell {F : ℝ → ℝ} (hF : Continuous F) (i : Fin 2) : MeasureTheory.IntegrableOn (fun (x : Homogenization.Vec 2) => F (x i)) (Torus.unitCell 2) MeasureTheory.volume

theorem AVenhance.Infra.Section3.spaceAvg_coordIntegral {F : ℝ → ℝ} (hF : Continuous F) (i : Fin 2) : (spaceAvg fun (x : Homogenization.Vec 2) => F (x i)) = ∫ (t : ℝ) in 0..1, F t

A coordinate-only continuous function averages to its one-dimensional unit-interval integral on the spatial cell.

theorem AVenhance.Infra.Section3.epsilon_inv_eq_ceil {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) : (epsilon β I.Λ m)⁻¹ = ↑⌈↑I.Λ ^ (q β ^ m / (q β - 1))⌉₊

At every positive scale the reciprocal cell length is the integer used to define epsilon.

theorem AVenhance.Infra.Section3.SpaceAverages.epsilon_frequency_pos {β : ℝ} (I : Ingredients β) {m : ℕ} : 0 < ⌈↑I.Λ ^ (q β ^ m / (q β - 1))⌉₊

theorem AVenhance.Infra.Section3.spaceAvg_sin_square_epsilon {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (i : Fin 2) : (spaceAvg fun (x : Homogenization.Vec 2) => Real.sin (2 * Real.pi * (epsilon β I.Λ m)⁻¹ * x i) ^ 2) = 1 / 2

The frequency 1/epsilon_m is a positive integer, so its sine and squared sine have the expected spatial averages.

theorem AVenhance.Infra.Section3.spaceAvg_sin_epsilon {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (i : Fin 2) : (spaceAvg fun (x : Homogenization.Vec 2) => Real.sin (2 * Real.pi * (epsilon β I.Λ m)⁻¹ * x i)) = 0