Jointly continuous periodic coefficients for the limiting spatial equation.

@[instance_reducible]

noncomputable def classicalJointMeasureSpace : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem classicalJointAddHaar : MeasureTheory.volume.IsAddHaarMeasure

theorem classicalJointProbability : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem classicalJointTorusProbability : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem classicalJointOneLeTwo : Fact (1 ≤ 2)

theorem AVenhance.Infra.Classical.GalerkinSmoothJointEquation.classicalJointWordPeriodic (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) (hper : IsZ2Periodic f) : IsZ2Periodic (classicalWordDerivative w f)

theorem AVenhance.Infra.Classical.GalerkinSmoothJointEquation.classicalToUnitTorus_isQuotientMap : Topology.IsQuotientMap (Torus.toUnitTorus 2)

noncomputable def AVenhance.Infra.Classical.classicalPeriodicFamilyJointPath {α : Type u_1} [TopologicalSpace α] (f : ↑(Set.Icc 0 1) → Homogenization.Vec 2 → α) (hf : Continuous (Function.uncurry f)) (hper : ∀ (t : ↑(Set.Icc 0 1)), Torus.IsZdPeriodic (f t)) : C(↑(Set.Icc 0 1) × UnitAddTorus (Fin 2), α)

Descend a jointly continuous periodic family to the time-space torus slab.

Equations

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

noncomputable def AVenhance.Infra.Classical.classicalGalerkinForcingJointPath (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) : C(↑(Set.Icc 0 1) × UnitAddTorus (Fin 2), ℂ)

The forcing, descended as a jointly continuous complex-valued torus path.

Equations

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

noncomputable def AVenhance.Infra.Classical.classicalGalerkinDriftCoordinateJointPath (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (j : Fin 2) : C(↑(Set.Icc 0 1) × UnitAddTorus (Fin 2), ℂ)

A coordinate of the smooth admissible drift, descended jointly in time and space.

Equations

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

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

The physical right-hand side of the limiting equation on the closed unit time slab.

Equations

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

theorem AVenhance.Infra.Classical.classicalGalerkinSmoothRhsJointPath_apply (φ : ℝ → 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 : UnitAddTorus (Fin 2)) : (classicalGalerkinSmoothRhsJointPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per) (t, x) = ↑(F (↑t) (Torus.unitTorusRepresentative 2 x)) + ↑κ * ↑(spaceLap (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t) (Torus.unitTorusRepresentative 2 x)) - ↑(Homogenization.vecDot (streamVel φ (↑t) (Torus.unitTorusRepresentative 2 x)) (spaceGrad (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t) (Torus.unitTorusRepresentative 2 x)))

noncomputable def AVenhance.Infra.Classical.classicalTorusFourierCoeffCLM (k : Fin 2 → ℤ) : C(UnitAddTorus (Fin 2), ℂ) →L[ℂ] ℂ

The continuous-map Fourier coefficient is a continuous linear functional.

Equations

• AVenhance.Infra.Classical.classicalTorusFourierCoeffCLM k = lp.evalCLM ℂ (fun (x : Fin 2 → ℤ) => ℂ) 2 k ∘SL ↑↑UnitAddTorus.mFourierBasis.repr ∘SL ContinuousMap.toLp 2 MeasureTheory.volume ℂ

theorem AVenhance.Infra.Classical.classicalTorusFourierCoeffCLM_apply (k : Fin 2 → ℤ) (f : C(UnitAddTorus (Fin 2), ℂ)) : (classicalTorusFourierCoeffCLM k) f = UnitAddTorus.mFourierCoeff (⇑f) k

theorem AVenhance.Infra.Classical.classicalJoint_mFourierCoeff_eq_smoothFourierCoeff {f : Homogenization.Vec 2 → ℂ} (hper : Torus.IsZdPeriodic f) (hf : Continuous f) (k : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (⇑{ toFun := Torus.periodicToTorus f, continuous_toFun := ⋯ }) k = Torus.smoothFourierCoeff f k

theorem AVenhance.Infra.Classical.classicalGalerkinWordFourierPath_fourierCoeff_eq_limit (φ : ℝ → 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 θ₀) (w : List (Fin 2)) (t : ↑(Set.Icc 0 1)) (k : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (⇑((classicalGalerkinWordFourierContinuousPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w).curry t)) k = (classicalGalerkinWordLimitFourierCoeffPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w k) t

The Fourier coefficient of every jointly continuous spatial derivative path is its Galerkin limit coefficient.

theorem AVenhance.Infra.Classical.classicalGalerkinSmoothRhsJointSlice_fourierCoeff_eq_physical (φ : ℝ → 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)) (k : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (⇑((classicalGalerkinSmoothRhsJointPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per).curry t)) k = UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin 2)) => ↑(Torus.periodicToTorus (fun (y : Homogenization.Vec 2) => F (↑t) y + (κ * spaceLap (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t) y - Homogenization.vecDot (streamVel φ (↑t) y) (spaceGrad (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t) y))) x)) k

def AVenhance.Infra.Classical.classicalGalerkinUnitSlabClamp (s : ℝ) : ↑(Set.Icc 0 1)

Clamp real time to the closed unit slab.

Equations

• AVenhance.Infra.Classical.classicalGalerkinUnitSlabClamp s = ⟨max 0 (min 1 s), ⋯⟩

theorem AVenhance.Infra.Classical.classicalGalerkinUnitSlabClamp_eq_of_mem {s : ℝ} (hs : s ∈ Set.Ioo 0 1) : classicalGalerkinUnitSlabClamp s = ⟨s, ⋯⟩

theorem AVenhance.Infra.Classical.classicalGalerkinWordFourierPath_fourierCoeff_hasDerivAt (φ : ℝ → 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 θ₀) (w : List (Fin 2)) (k : Fin 2 → ℤ) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : HasDerivAt (fun (s : ℝ) => UnitAddTorus.mFourierCoeff (⇑((classicalGalerkinWordFourierContinuousPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w).curry (classicalGalerkinUnitSlabClamp s))) k) (classicalGalerkinWordFourierMultiplier k w * UnitAddTorus.mFourierCoeff (⇑((classicalGalerkinSmoothRhsJointPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per).curry ⟨t, ⋯⟩)) k) t

The Fourier coefficients of every spatial derivative path satisfy the differentiated limiting equation on the interior of the unit time slab.

theorem AVenhance.Infra.Classical.GalerkinSmoothJointEquation.continuous_classicalGalerkinUnitSlabClamp : Continuous classicalGalerkinUnitSlabClamp