Fourier test density connecting the analytic App C dual tests to the smooth-test norm. All approximants are actual finite real trig sums.

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

theorem AVenhance.Infra.Section5.TestDensity.gradient_avg (f : Homogenization.Vec 2 → ℝ) : Ergodic.gradientL2SquaredAverage f = gradNormSq (spaceGrad f)

theorem AVenhance.Infra.Section5.TestDensity.continuous_L2 {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : Homogenization.MemL2On unitCube f

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

noncomputable def AVenhance.Infra.Section5.testFourierCutoff (f : Homogenization.Vec 2 → ℝ) (N : ℕ) : Homogenization.Vec 2 → ℝ

The actual real Fourier truncation on the supremum-norm lattice ball.

Equations

• AVenhance.Infra.Section5.testFourierCutoff f N = AVenhance.Infra.Ergodic.lowProjection f N

theorem AVenhance.Infra.Section5.testFourierCutoff_analytic (f : Homogenization.Vec 2 → ℝ) (N : ℕ) : ContDiff ℝ ⊤ (testFourierCutoff f N)

theorem AVenhance.Infra.Section5.testFourierCutoff_periodic (f : Homogenization.Vec 2 → ℝ) (N : ℕ) : IsZ2Periodic (testFourierCutoff f N)

theorem AVenhance.Infra.Section5.TestDensity.cutoff_coeff {f : Homogenization.Vec 2 → ℝ} (_hf : Continuous f) (N : ℕ) (k : Fin 2 → ℤ) : Torus.smoothFourierCoeff (fun (x : Homogenization.Vec 2) => ↑(testFourierCutoff f N x)) k = if k ∈ Ergodic.frequencyBall N then Torus.smoothFourierCoeff (fun (x : Homogenization.Vec 2) => ↑(f x)) k else 0

theorem AVenhance.Infra.Section5.TestDensity.tail_coeff {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) (N : ℕ) (k : Fin 2 → ℤ) : Torus.smoothFourierCoeff (fun (x : Homogenization.Vec 2) => ↑(f x - testFourierCutoff f N x)) k = if k ∈ Ergodic.frequencyBall N then 0 else Torus.smoothFourierCoeff (fun (x : Homogenization.Vec 2) => ↑(f x)) k

theorem AVenhance.Infra.Section5.TestDensity.eventually_frequency_mem (k : Fin 2 → ℤ) : ∀ᶠ (N : ℕ) in Filter.atTop, k ∈ Ergodic.frequencyBall N

theorem AVenhance.Infra.Section5.TestDensity.tail_tsum_tendsto {a : (Fin 2 → ℤ) → ℝ} (ha : Summable a) (hpos : ∀ (k : Fin 2 → ℤ), 0 ≤ a k) : Filter.Tendsto (fun (N : ℕ) => ∑' (k : Fin 2 → ℤ), if k ∈ Ergodic.frequencyBall N then 0 else a k) Filter.atTop (nhds 0)

theorem AVenhance.Infra.Section5.testFourierCutoff_L2_error_tendsto {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) : Filter.Tendsto (fun (N : ℕ) => l2NormSq fun (x : Homogenization.Vec 2) => f x - testFourierCutoff f N x) Filter.atTop (nhds 0)

Real Parseval gives convergence of the value error to zero in L2.

theorem AVenhance.Infra.Section5.TestDensity.gradient_coeff_cutoff {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hp : IsZ2Periodic f) (N : ℕ) (i : Fin 2) (k : Fin 2 → ℤ) : Torus.smoothFourierCoeff (fun (x : Homogenization.Vec 2) => ↑(spaceGrad (testFourierCutoff f N) x i)) k = if k ∈ Ergodic.frequencyBall N then Torus.smoothFourierCoeff (fun (x : Homogenization.Vec 2) => ↑(spaceGrad f x i)) k else 0

theorem AVenhance.Infra.Section5.TestDensity.grad_component_cont {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (i : Fin 2) : Continuous fun (x : Homogenization.Vec 2) => spaceGrad f x i

theorem AVenhance.Infra.Section5.TestDensity.gradient_energy_parseval {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) : HasSum (fun (k : Fin 2 → ℤ) => ∑ i : Fin 2, ‖Torus.smoothFourierCoeff (fun (x : Homogenization.Vec 2) => ↑(spaceGrad f x i)) k‖ ^ 2) (gradNormSq (spaceGrad f))

theorem AVenhance.Infra.Section5.testFourierCutoff_gradient_le {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hp : IsZ2Periodic f) (N : ℕ) : gradNormSq (spaceGrad (testFourierCutoff f N)) ≤ gradNormSq (spaceGrad f)

Orthogonal truncation never increases gradient energy. Thus normalized tests stay normalized without an artificial rescaling.

theorem AVenhance.Infra.Section5.testFourierCutoff_gradient_error_tendsto {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hp : IsZ2Periodic f) : Filter.Tendsto (fun (N : ℕ) => gradNormSq (spaceGrad fun (x : Homogenization.Vec 2) => f x - testFourierCutoff f N x)) Filter.atTop (nhds 0)

The Fourier derivative multiplier and Parseval give gradient-error convergence, not merely convergence of values.

theorem AVenhance.Infra.Section5.TestDensity.coeff_zero (f : Homogenization.Vec 2 → ℝ) (hf : Continuous f) : Torus.smoothFourierCoeff (fun (x : Homogenization.Vec 2) => ↑(f x)) 0 = ↑(∫ (x : Homogenization.Vec 2) in unitCube, f x)

theorem AVenhance.Infra.Section5.testFourierCutoff_mean (f : Homogenization.Vec 2 → ℝ) (hf : Continuous f) (N : ℕ) : ∫ (x : Homogenization.Vec 2) in unitCube, testFourierCutoff f N x = ∫ (x : Homogenization.Vec 2) in unitCube, f x

The zero coefficient is retained, so the actual cell mean is preserved.

theorem AVenhance.Infra.Section5.TestDensity.pairing_error_bound {g u : Homogenization.Vec 2 → ℝ} (hg : Homogenization.MemL2On unitCube g) (hu : Continuous u) : |∫ (x : Homogenization.Vec 2) in unitCube, g x * u x| ≤ √(l2NormSq g) * √(l2NormSq u)

L2 Cauchy–Schwarz in value carriers.

theorem AVenhance.Infra.Section5.testFourierCutoff_pairing_tendsto {g f : Homogenization.Vec 2 → ℝ} (hg : Homogenization.MemL2On unitCube g) (hf : ContDiff ℝ 1 f) : Filter.Tendsto (fun (N : ℕ) => ∫ (x : Homogenization.Vec 2) in unitCube, g x * testFourierCutoff f N x) Filter.atTop (nhds (∫ (x : Homogenization.Vec 2) in unitCube, g x * f x))

Every L2 datum pairs continuously with the actual Fourier truncations.

theorem AVenhance.Infra.Section5.testFourierCutoff_admissible {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hp : IsZ2Periodic f) (hm : Homogenization.MeanZeroOn unitCube f) (hn : gradNormSq (spaceGrad f) ≤ 1) (N : ℕ) : ContDiff ℝ ⊤ (testFourierCutoff f N) ∧ Ergodic.IsZPeriodic (testFourierCutoff f N) ∧ Ergodic.cellAverage (testFourierCutoff f N) = 0 ∧ Ergodic.gradientL2SquaredAverage (testFourierCutoff f N) ≤ 1

Centred Fourier approximants retain analytic regularity, periodicity, zero mean and the gradient normalization.

theorem AVenhance.Infra.Section5.hMinusOneNorm_eq_ergodic {g : Homogenization.Vec 2 → ℝ} (hg : Homogenization.MemL2On unitCube g) (hm : Homogenization.MeanZeroOn unitCube g) : hMinusOneNorm g = Ergodic.homogeneousHMinusOneNorm g

Density closes the formerly missing upper-bound direction. No periodicity of the L2 datum is needed for equality of these cell dual suprema.

theorem AVenhance.Infra.Section5.TestDensity.product_L2 {f g : Homogenization.Vec 2 → ℝ} (hf : Continuous f) (hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume) (hg2 : MeasureTheory.LocallyIntegrable (fun (x : Homogenization.Vec 2) => |g x| ^ 2) MeasureTheory.volume) : Homogenization.MemL2On unitCube fun (x : Homogenization.Vec 2) => f x * g x

def AVenhance.Infra.Section5.TestDensity.densityFlowHomeomorph (X : Ergodic.PeriodicVolumePreservingDiffeomorphism 2) : Homogenization.Vec 2 ≃ₜ Homogenization.Vec 2

Homeomorphism underlying a periodic volume-preserving flow for test-function density.

Equations

• AVenhance.Infra.Section5.TestDensity.densityFlowHomeomorph X = { toFun := X.toFun, invFun := X.invFun, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem AVenhance.Infra.Section5.TestDensity.flow_local_integrable (X : Ergodic.PeriodicVolumePreservingDiffeomorphism 2) {g : Homogenization.Vec 2 → ℝ} (hg : MeasureTheory.LocallyIntegrable g MeasureTheory.volume) : MeasureTheory.LocallyIntegrable (fun (x : Homogenization.Vec 2) => g (X.invFun x)) MeasureTheory.volume