Periodizing compact Euclidean tests against the periodic weak gradient

The lattice of integer translations has a compact fundamental cell. Compact support makes the periodization locally a finite sum, so it retains the smoothness of the original test.

@[reducible, inline]

abbrev AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.PeriodLattice : Submodule ℤ (Fin 2 → ℝ)

Integer span of the coordinate basis, defining the period lattice.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.PeriodLattice = Submodule.span ℤ (Set.range ⇑(Pi.basisFun ℝ (Fin 2)))

@[reducible, inline]

abbrev AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.PeriodTranslations : AddSubgroup (Fin 2 → ℝ)

Additive group of translations by vectors in the period lattice.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.PeriodTranslations = AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.PeriodLattice.toAddSubgroup

def AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.PeriodCell : Set (Homogenization.Vec 2)

Fundamental cell for translations by the coordinate period lattice.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.PeriodCell = ZSpan.fundamentalDomain (Pi.basisFun ℝ (Fin 2))

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodTranslations_fundamentalDomain : MeasureTheory.IsAddFundamentalDomain (↥PeriodTranslations) PeriodCell MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodCell_ae_unitCube : PeriodCell =ᵐ[MeasureTheory.volume] unitCube

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodTranslation_integerVector (z : ↥PeriodTranslations) : ∃ (k : Fin 2 → ℤ), ↑z = latticeShift k

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodTranslationIndex (z : ↥PeriodTranslations) : Fin 2 → ℤ

Integer coordinate vector representing a period translation.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodTranslationIndex z = Classical.choose ⋯

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodTranslationIndex_spec (z : ↥PeriodTranslations) : ↑z = latticeShift (periodTranslationIndex z)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodLattice_countable : (↑PeriodLattice).Countable

instance AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodTranslations_countable : Countable ↥PeriodTranslations

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodCell_measurable : MeasurableSet PeriodCell

instance AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodCell_finiteMeasure : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict PeriodCell)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodCell_memLp {g : Homogenization.Vec 2 → ℝ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict unitCube)) : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict PeriodCell)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodCell_translate_memLp {g : Homogenization.Vec 2 → ℝ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict PeriodCell)) (hperiodic : IsZ2Periodic g) (z : ↥PeriodTranslations) : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (↑z +ᵥ PeriodCell))

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodCell_translate_preimage (z : ↥PeriodTranslations) : (fun (x : Homogenization.Vec 2) => x - ↑z) ⁻¹' PeriodCell = ↑z +ᵥ PeriodCell

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodCell_translate_measurable (z : ↥PeriodTranslations) : MeasurableSet (↑z +ᵥ PeriodCell)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodCell_translate_finiteMeasure (z : ↥PeriodTranslations) : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict (↑z +ᵥ PeriodCell))

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodCell_translate_integrable {g : Homogenization.Vec 2 → ℝ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict unitCube)) (hperiodic : IsZ2Periodic g) (z : ↥PeriodTranslations) : MeasureTheory.IntegrableOn g (↑z +ᵥ PeriodCell) MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.continuous_compact_support_norm_bound {w : Homogenization.Vec 2 → ℝ} (hw : Continuous w) (hws : HasCompactSupport w) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Homogenization.Vec 2), ‖w x‖ ≤ C

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.integrableOn_periodic_mul_continuous_compact {g w : Homogenization.Vec 2 → ℝ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict unitCube)) (hperiodic : IsZ2Periodic g) (hw : Continuous w) (hws : HasCompactSupport w) (z : ↥PeriodTranslations) : MeasureTheory.IntegrableOn (fun (x : Homogenization.Vec 2) => g x * w x) (↑z +ᵥ PeriodCell) MeasureTheory.volume

def AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodCellClosure : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodCellClosure = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodCellClosure_compact : IsCompact periodCellClosure

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodCell_subset_closure : PeriodCell ⊆ periodCellClosure

noncomputable def AVenhance.Infra.Parabolic.FourierGalerkin.compactTestPeriodization (φ : Homogenization.Vec 2 → ℝ) : Homogenization.Vec 2 → ℝ

Periodize a compactly supported test function by summing its lattice translates.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.compactTestPeriodization φ x = ∑ᶠ (z : ↥AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.PeriodTranslations), φ (x + ↑z)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.periodized_family_locallyFinite {φ : Homogenization.Vec 2 → ℝ} (hφ : HasCompactSupport φ) : LocallyFinite fun (z : ↥PeriodTranslations) => {x : Homogenization.Vec 2 | φ (x + ↑z) ≠ 0}

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.integral_periodic_mul_compact_eq_cell_periodization {g w : Homogenization.Vec 2 → ℝ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict unitCube)) (hperiodic : IsZ2Periodic g) (hw : Continuous w) (hws : HasCompactSupport w) : MeasureTheory.Integrable (fun (x : Homogenization.Vec 2) => g x * w x) MeasureTheory.volume ∧ ∫ (x : Homogenization.Vec 2), g x * w x = ∫ (x : Homogenization.Vec 2) in PeriodCell, g x * compactTestPeriodization w x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.compactTestPeriodization_contDiff {φ : Homogenization.Vec 2 → ℝ} (hφ : HasCompactSupport φ) (hφsmooth : ContDiff ℝ (↑⊤) φ) : ContDiff ℝ (↑⊤) (compactTestPeriodization φ)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.WeakGradientPeriodization.compactTestPeriodization_periodic_translation (φ : Homogenization.Vec 2 → ℝ) (z : ↥PeriodTranslations) (x : Homogenization.Vec 2) : compactTestPeriodization φ (x + ↑z) = compactTestPeriodization φ x

theorem AVenhance.Infra.Parabolic.FourierGalerkin.compactTestPeriodization_periodic {φ : Homogenization.Vec 2 → ℝ} : IsZ2Periodic (compactTestPeriodization φ)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.compactTestPeriodization_spaceGrad_eq {φ : Homogenization.Vec 2 → ℝ} (hφ : HasCompactSupport φ) (hφsmooth : ContDiff ℝ (↑⊤) φ) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (compactTestPeriodization φ) x i = ∑ᶠ (z : ↥WeakGradientPeriodization.PeriodTranslations), spaceGrad φ (x + ↑z) i

theorem AVenhance.Infra.Parabolic.FourierGalerkin.hasWeakGradientOn_of_realFourierModes {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict unitCube)) (hDu : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (x : Homogenization.Vec 2) => Du x i) 2 (MeasureTheory.volume.restrict unitCube)) (hperiodicU : IsZ2Periodic u) (hperiodicDu : IsZ2Periodic Du) (hmode : ∀ (i : Fin 2) (N : ℕ) (j : Fin (RealFourierDimension N)), ∫ (x : Homogenization.Vec 2) in unitCube, u x * spaceGrad (realFourierModeAmbient N ((realFourierIndexEquivFin N).symm j)) x i = -∫ (x : Homogenization.Vec 2) in unitCube, Du x i * realFourierModeAmbient N ((realFourierIndexEquivFin N).symm j) x) : Homogenization.HasWeakGradientOn Set.univ u Du

Fourier weak-derivative identities imply the global weak-gradient clause. A compact Euclidean test is periodized, the cell identity is applied to that smooth periodic test, and the two resulting cell pairings are unfolded back to ℝ².

theorem AVenhance.Infra.Parabolic.FourierGalerkin.periodic_compact_pairing_integrable {u w : Homogenization.Vec 2 → ℝ} (hu : Homogenization.MemL2On unitCube u) (hperiodic : IsZ2Periodic u) (hw : Continuous w) (hws : HasCompactSupport w) : MeasureTheory.Integrable (fun (x : Homogenization.Vec 2) => u x * w x) MeasureTheory.volume

A periodic cell-L² function paired with a continuous compactly supported test is globally integrable. This is the integrability bridge needed to take linear combinations of global weak derivative identities.