Real-valued periodic integration by parts for Galerkin tests

This bridge specializes the landed complex torus-calculus theorem to the real gradient and the open unit-cell carrier used by the parabolic weak formulation.

def AVenhance.Infra.Parabolic.FourierGalerkin.TorusBridge.closedCell : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

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

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TorusBridge.isCompact_closedCell : IsCompact closedCell

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TorusBridge.unitCell_subset_closedCell : Torus.unitCell 2 ⊆ closedCell

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TorusBridge.continuousOn_unitCell_integrable {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f (Torus.unitCell 2) MeasureTheory.volume

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TorusBridge.realToComplex_periodic {f : Homogenization.Vec 2 → ℝ} (hperiodic : IsZ2Periodic f) : Torus.IsZdPeriodic (Torus.realToComplex f)

theorem AVenhance.Infra.Parabolic.FourierGalerkin.TorusBridge.continuous_spaceGrad_coord {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ ⊤ f) (i : Fin 2) : Continuous fun (x : Homogenization.Vec 2) => spaceGrad f x i