The smooth Fourier representative is real-valued, as inherited from the real Galerkin paths.

theorem AVenhance.Infra.Classical.classicalSmoothRealOneLeTwo : Fact (1 ≤ 2)

@[instance_reducible]

noncomputable def AVenhance.Infra.Classical.classicalSmoothRealMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

Use normalized Haar measure on the unit circle for periodic integrals.

Equations

• AVenhance.Infra.Classical.classicalSmoothRealMeasureSpaceUnitAddCircle = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem AVenhance.Infra.Classical.classicalSmoothRealMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem AVenhance.Infra.Classical.classicalSmoothRealProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Classical.classicalGalerkinFourierContinuousLimit_im_eq_zero (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (t : ↑(Set.Icc 0 1)) (x : Parabolic.FourierGalerkin.Torus) : ((classicalGalerkinFourierContinuousLimit φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t) x).im = 0

The continuous Fourier representative has zero imaginary part: its L² class is the complexification of the real-valued Galerkin limit.

theorem AVenhance.Infra.Classical.classicalGalerkinSmoothLift_im_eq_zero (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (t : ↑(Set.Icc 0 1)) (x : Homogenization.Vec 2) : (classicalGalerkinSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t x).im = 0

The pointwise smooth Fourier lift is real-valued on every spatial slice.

noncomputable def AVenhance.Infra.Classical.classicalGalerkinRealSmoothLift (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (t : ↑(Set.Icc 0 1)) : Homogenization.Vec 2 → ℝ

A real-valued version of the smooth Galerkin lift.

Equations

• AVenhance.Infra.Classical.classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t x = (AVenhance.Infra.Classical.classicalGalerkinSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t x).re

theorem AVenhance.Infra.Classical.classicalGalerkinRealSmoothLift_contDiff (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (t : ↑(Set.Icc 0 1)) : ContDiff ℝ (↑⊤) (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t)

theorem AVenhance.Infra.Classical.classicalGalerkinRealSmoothLift_periodic (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (hθ₀per : IsZ2Periodic θ₀) (t : ↑(Set.Icc 0 1)) : IsZ2Periodic (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t)