Joint time continuity of the smooth Fourier representatives.

@[instance_reducible]

noncomputable def classicalSmoothTimeMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem classicalSmoothTimeMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem classicalSmoothTimeProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Classical.ForcedGalerkinData.hasDerivAt_on_Ioo_of_continuousOn {E : Type u_1} {G : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup G] [NormedSpace ℝ G] (D : ForcedGalerkinData E G) (u : C(↑(Set.Icc 0 1), E)) (hu : D.ode.IsSolution u) (hA : ContinuousOn D.weak.coefficient (Set.Icc 0 1)) (hf : ContinuousOn D.forcing (Set.Icc 0 1)) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : HasDerivAt (ODE.extendCurve hasDerivAt_on_Ioo_of_continuousOn._proof_1 u) ((D.weak.coefficient t) (ODE.extendCurve hasDerivAt_on_Ioo_of_continuousOn._proof_1 u t) + D.forcing t) t

The integral equation gives a classical time derivative in the open slab when the operator and forcing are continuous on the slab. This version accommodates the zero extension in the measurable ODE interface, whose coefficient need not be continuous outside [0,1].

theorem AVenhance.Infra.Classical.GalerkinSmoothTime.classicalSummable_of_norm_le_majorant {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [CompleteSpace E] (f : ι → E) (g : ι → ℝ) (hg : Summable g) (hfg : ∀ (i : ι), ‖f i‖ ≤ g i) (_hg0 : ∀ (i : ι), 0 ≤ g i) : Summable f

@[irreducible]

noncomputable def AVenhance.Infra.Classical.classicalGalerkinFourierJointTerm (φ : ℝ → 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 θ₀) (k : Fin 2 → ℤ) : C(↑(Set.Icc 0 1) × UnitAddTorus (Fin 2), ℂ)

One Fourier mode as a continuous function jointly in time and torus position.

Equations

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

theorem AVenhance.Infra.Classical.GalerkinSmoothTime.classicalGalerkinFourierJointTerm_norm_le (φ : ℝ → 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 θ₀) (k : Fin 2 → ℤ) : ‖classicalGalerkinFourierJointTerm φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per k‖ ≤ classicalGalerkinFourierCoefficientBound φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per 0 * classicalScaledTorusFrequencyWeight k

theorem AVenhance.Infra.Classical.GalerkinSmoothTime.classicalGalerkinFourierJointTerm_summable (φ : ℝ → 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 θ₀) : Summable (classicalGalerkinFourierJointTerm φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per)