Real-valued d = 2 corollaries in the paper carriers.

noncomputable def AVenhance.Infra.Torus.realToComplex (f : Homogenization.Vec 2 → ℝ) : Homogenization.Vec 2 → ℂ

Regard a real-valued Euclidean function as complex-valued.

Equations

• AVenhance.Infra.Torus.realToComplex f = ⇑Complex.ofRealCLM ∘ f

theorem AVenhance.Infra.Torus.coordDeriv_realToComplex {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (i : Fin 2) (x : Homogenization.Vec 2) : coordDeriv i (realToComplex f) x = ↑(spaceGrad f x i)

The complex coordinate derivative of the real cast is the cast of the classical gradient.

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

def AVenhance.Infra.Torus.FrozenBridge.closedUnitSquare : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

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

theorem AVenhance.Infra.Torus.FrozenBridge.real_integrableOn_unitCell {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f (unitCell 2) MeasureTheory.volume

theorem AVenhance.Infra.Torus.FrozenBridge.realToComplex_meanZero {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) (hmean : ∫ (x : Homogenization.Vec 2) in unitCube, f x = 0) : ∫ (x : Homogenization.Vec 2) in unitCell 2, realToComplex f x = 0

theorem AVenhance.Infra.Torus.FrozenBridge.realToComplex_energy {f : Homogenization.Vec 2 → ℝ} : ∫ (x : Homogenization.Vec 2) in unitCell 2, ‖realToComplex f x‖ ^ 2 = l2NormSq f

theorem AVenhance.Infra.Torus.FrozenBridge.realToComplex_gradient_energy {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) : ∫ (x : Homogenization.Vec 2) in unitCell 2, ∑ i : Fin 2, ‖coordDeriv i (realToComplex f) x‖ ^ 2 = gradNormSq (spaceGrad f)

theorem AVenhance.Infra.Torus.hasSum_sq_realToComplexFourierCoeff {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) : HasSum (fun (k : Fin 2 → ℤ) => ‖smoothFourierCoeff (realToComplex f) k‖ ^ 2) (l2NormSq f)

The real d = 2 scalar Parseval identity in the l2NormSq carrier.

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

The real d = 2 gradient Parseval identity in the gradNormSq carrier.

theorem AVenhance.Infra.Torus.smoothFourierCoeff_spaceGrad {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hperiodic : IsZ2Periodic f) (i : Fin 2) (k : Fin 2 → ℤ) : smoothFourierCoeff (fun (x : Homogenization.Vec 2) => ↑(spaceGrad f x i)) k = 2 * ↑Real.pi * Complex.I * ↑(k i) * smoothFourierCoeff (realToComplex f) k

Fourier multiplier formula for each component of the real gradient.

theorem AVenhance.Infra.Torus.l2NormSq_le_fourierPoincare {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hperiodic : IsZ2Periodic f) (hmean : ∫ (x : Homogenization.Vec 2) in unitCube, f x = 0) : l2NormSq f ≤ (4 * Real.pi ^ 2)⁻¹ * gradNormSq (spaceGrad f)

Mean-zero Poincare inequality in the d = 2 carriers.