Continuity and time integrability of the smooth forcing in each Fourier Galerkin system.

@[instance_reducible]

noncomputable def classicalForcingMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

• classicalForcingMeasureSpaceUnitAddCircle = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem classicalForcingMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem classicalForcingProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem classicalForcingProbabilityTorus : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

def AVenhance.Infra.Classical.GalerkinForcing.forcingClosedCell : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Classical.GalerkinForcing.forcingClosedCell = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Classical.GalerkinForcing.unitCell_ae_eq_forcingClosedCell : Torus.unitCell 2 =ᵐ[MeasureTheory.volume] forcingClosedCell

theorem AVenhance.Infra.Classical.GalerkinForcing.forcingContinuousExtension (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) : Continuous (Function.uncurry fun (t : ℝ) (x : Homogenization.Vec 2) => F (max t 0) x)

noncomputable def AVenhance.Infra.Classical.classicalForcingCoefficients (N : ℕ) (F : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)

Fourier projection of a smooth half-line forcing, extended continuously to negative times by clamping the time coordinate at zero.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Classical.GalerkinForcing.classicalForcingCoefficient_eq_closedCellIntegral (N : ℕ) (F : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (i : Fin (Parabolic.FourierGalerkin.RealFourierDimension N)) : (classicalForcingCoefficients N F t).ofLp i = ∫ (x : Homogenization.Vec 2) in forcingClosedCell, F (max t 0) x * Parabolic.FourierGalerkin.realFourierModeAmbient N ((Parabolic.FourierGalerkin.realFourierIndexEquivFin N).symm i) x

theorem AVenhance.Infra.Classical.classicalForcingCoefficients_continuous (N : ℕ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) : Continuous (classicalForcingCoefficients N F)

The coefficient forcing path is continuous, hence interval integrable on every compact time interval.

theorem AVenhance.Infra.Classical.classicalForcingCoefficients_intervalIntegrable (N : ℕ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) : IntervalIntegrable (classicalForcingCoefficients N F) MeasureTheory.volume 0 1