Uniform Cauchy convergence of the time derivatives of finite Fourier modes.

theorem classicalTimeCauchyOneLeTwo : Fact (1 ≤ 2)

@[instance_reducible]

noncomputable def classicalTimeCauchyMeasureSpace : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem classicalTimeCauchyAddHaar : MeasureTheory.volume.IsAddHaarMeasure

theorem classicalTimeCauchyProbability : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem classicalTimeCauchyTorusProbability : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Classical.GalerkinSmoothTimeCauchy.classicalTimeCauchyTransport_contDiff (b : Homogenization.Vec 2 → Homogenization.Vec 2) (u : Homogenization.Vec 2 → ℝ) (hb : ContDiff ℝ (↑⊤) b) (hu : ContDiff ℝ (↑⊤) u) : ContDiff ℝ (↑⊤) (classicalTransport b u)

theorem AVenhance.Infra.Classical.GalerkinSmoothTimeCauchy.classicalTimeCauchyTransport_periodic (b : Homogenization.Vec 2 → Homogenization.Vec 2) (u : Homogenization.Vec 2 → ℝ) (hb : IsZ2Periodic b) (hu : IsZ2Periodic u) : IsZ2Periodic (classicalTransport b u)

theorem AVenhance.Infra.Classical.GalerkinSmoothTimeCauchy.classicalTimeCauchySpaceLap_contDiff (u : Homogenization.Vec 2 → ℝ) (hu : ContDiff ℝ (↑⊤) u) : ContDiff ℝ (↑⊤) (spaceLap u)

theorem AVenhance.Infra.Classical.GalerkinSmoothTimeCauchy.classicalTimeCauchySpaceLap_periodic (u : Homogenization.Vec 2 → ℝ) (hu : IsZ2Periodic u) : IsZ2Periodic (spaceLap u)

theorem AVenhance.Infra.Classical.classicalGalerkinFiniteFourierDerivativePath_eq_spatialRhs_closed (φ : ℝ → 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 ℝ (↑⊤) θ₀) (N : ℕ) (k : Fin 2 → ℤ) (hk : Parabolic.FourierGalerkin.frequencyPair k ∈ Parabolic.FourierGalerkin.symmetricFrequencyBox N) (t : ↑(Set.Icc 0 1)) : (classicalGalerkinFiniteFourierDerivativePath φ hφ κ hκ F hF θ₀ hθ₀ N k) t = UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(Torus.periodicToTorus (fun (y : Homogenization.Vec 2) => F (↑t) y + (κ * spaceLap (realFourierModeAmbientExpansion N ((classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N) t)) y - classicalTransport (streamVel φ ↑t) (realFourierModeAmbientExpansion N ((classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N) t)) y)) x)) k

theorem AVenhance.Infra.Classical.classicalGalerkinFiniteFourierDerivativePath_eq_spatialRhs_decomp (φ : ℝ → 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 ℝ (↑⊤) θ₀) (N : ℕ) (k : Fin 2 → ℤ) (hk : Parabolic.FourierGalerkin.frequencyPair k ∈ Parabolic.FourierGalerkin.symmetricFrequencyBox N) (t : ↑(Set.Icc 0 1)) : (classicalGalerkinFiniteFourierDerivativePath φ hφ κ hκ F hF θ₀ hθ₀ N k) t = ↑κ * UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(Torus.periodicToTorus (spaceLap (realFourierModeAmbientExpansion N ((classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N) t))) x)) k - UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(Torus.periodicToTorus (classicalTransport (streamVel φ ↑t) (realFourierModeAmbientExpansion N ((classicalGalerkinCoefficientPath φ hφ κ hκ F hF θ₀ hθ₀ N) t))) x)) k + UnitAddTorus.mFourierCoeff (fun (x : Parabolic.FourierGalerkin.Torus) => ↑(Torus.periodicToTorus (F ↑t) x)) k

theorem AVenhance.Infra.Classical.classicalGalerkinFiniteFourierDerivativePath_cauchy (φ : ℝ → 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 → ℤ) : CauchySeq fun (N : ℕ) => classicalGalerkinFiniteFourierDerivativePath φ hφ κ hκ F hF θ₀ hθ₀ N k

noncomputable def AVenhance.Infra.Classical.classicalGalerkinFiniteFourierDerivativePathLimit (φ : ℝ → 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), ℂ)

Limit of the time derivatives of the finite Fourier Galerkin paths.

Equations

• AVenhance.Infra.Classical.classicalGalerkinFiniteFourierDerivativePathLimit φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per k = Classical.choose ⋯

theorem AVenhance.Infra.Classical.classicalGalerkinFiniteFourierDerivativePathLimit_tendsto (φ : ℝ → 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 → ℤ) : Filter.Tendsto (fun (N : ℕ) => classicalGalerkinFiniteFourierDerivativePath φ hφ κ hκ F hF θ₀ hθ₀ N k) Filter.atTop (nhds (classicalGalerkinFiniteFourierDerivativePathLimit φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per k))

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

Clamp a real time to the closed unit time interval.

Equations

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

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

theorem AVenhance.Infra.Classical.classicalGalerkinLimitFourierCoeffPath_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 θ₀) (k : Fin 2 → ℤ) {t : ℝ} (ht : t ∈ Set.Ioo 0 1) : HasDerivAt (fun (s : ℝ) => (classicalGalerkinLimitFourierCoeffPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per k) (classicalTimeCauchyClamp s)) ((classicalGalerkinFiniteFourierDerivativePathLimit φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per k) (classicalTimeCauchyClamp t)) t

The limiting Fourier coefficient is differentiable on the interior slab; its derivative is the uniform limit of the finite Galerkin coefficient derivatives.