Fourier and time-rescaling adapters for the classical Galerkin limit paths.

The strong limit constructed in Infra/Classical/GalerkinSmoothLimit has type C(Icc (0 : ℝ) 1, ScalarTorusL2). These lemmas identify such limits from their Fourier cutoffs and compare them on nested physical-time intervals.

theorem AVenhance.Infra.Classical.classicalGalerkinLimitPath_eq_under_timeMap (a b : ℕ → C(↑(Set.Icc 0 1), ↥Parabolic.FourierGalerkin.ScalarTorusL2)) (u v : C(↑(Set.Icc 0 1), ↥Parabolic.FourierGalerkin.ScalarTorusL2)) (ha : Filter.Tendsto a Filter.atTop (nhds u)) (hb : Filter.Tendsto b Filter.atTop (nhds v)) (σ : C(↑(Set.Icc 0 1), ↑(Set.Icc 0 1))) (hfinite : ∀ (N : ℕ) (s : ↑(Set.Icc 0 1)), (a N) s = (b N) (σ s)) (s : ↑(Set.Icc 0 1)) : u s = v (σ s)

Limits of finite Galerkin paths preserve equality under a continuous time reparameterization. This is the comparison step used when two scaled unit-slab constructions describe the same physical times.

noncomputable def AVenhance.Infra.Classical.classicalGalerkinNestedTimeMap (T S : ℝ) (hT : 0 < T) (hTS : T ≤ S) : C(↑(Set.Icc 0 1), ↑(Set.Icc 0 1))

Rescale the shorter unit slab into a longer unit slab: equal normalized points represent the same physical time when the first construction has horizon T and the second horizon S.

Equations

• AVenhance.Infra.Classical.classicalGalerkinNestedTimeMap T S hT hTS = { toFun := fun (s : ↑(Set.Icc 0 1)) => ⟨T / S * ↑s, ⋯⟩, continuous_toFun := ⋯ }

theorem AVenhance.Infra.Classical.classicalGalerkinNestedTimeMap_physicalTime (T S : ℝ) (hT : 0 < T) (hTS : T ≤ S) (s : ↑(Set.Icc 0 1)) : S * ↑((classicalGalerkinNestedTimeMap T S hT hTS) s) = T * ↑s

The nested unit-slab map preserves physical time.

theorem AVenhance.Infra.Classical.classicalGalerkinFiniteODEPath_rescale {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (T S : ℝ) (hT : 0 < T) (hTS : T ≤ S) (DT DS : ODE.LinearODEData 0 1 classicalGalerkinFiniteODEPath_rescale._proof_1) (uT uS : C(↑(Set.Icc 0 1), E)) (huT : DT.IsSolution uT) (huS : DS.IsSolution uS) (hy₀ : DT.y₀ = DS.y₀) (hA : ∀ t ∈ Set.Icc 0 1, DT.A t = (T / S) • DS.A (T / S * t)) (hf : ∀ t ∈ Set.Icc 0 1, DT.f t = (T / S) • DS.f (T / S * t)) (s : ↑(Set.Icc 0 1)) : uT s = uS ((classicalGalerkinNestedTimeMap T S hT hTS) s)

Finite-dimensional linear Galerkin paths agree on a nested interval when their operators and forcings are related by the physical-time rescaling. This discharges the finite-path premise in classicalGalerkinIncreasingHorizon_consistent for the horizon-rescaled Galerkin systems.

noncomputable def AVenhance.Infra.Classical.classicalGalerkinCoefficientScalarPath (N : ℕ) (u : C(↑(Set.Icc 0 1), Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N))) : C(↑(Set.Icc 0 1), ↥Parabolic.FourierGalerkin.ScalarTorusL2)

View a finite real-Fourier coefficient path as a continuous scalar torus L² path.

Equations

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

theorem AVenhance.Infra.Classical.classicalGalerkinIncreasingHorizon_consistent_of_finiteODE (T S : ℝ) (hT : 0 < T) (hTS : T ≤ S) (DT DS : (N : ℕ) → ODE.LinearODEData 0 1 classicalGalerkinFiniteODEPath_rescale._proof_1) (uT uS : (N : ℕ) → C(↑(Set.Icc 0 1), Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N))) (hsolT : ∀ (N : ℕ), (DT N).IsSolution (uT N)) (hsolS : ∀ (N : ℕ), (DS N).IsSolution (uS N)) (hy₀ : ∀ (N : ℕ), (DT N).y₀ = (DS N).y₀) (hA : ∀ (N : ℕ), ∀ t ∈ Set.Icc 0 1, (DT N).A t = (T / S) • (DS N).A (T / S * t)) (hf : ∀ (N : ℕ), ∀ t ∈ Set.Icc 0 1, (DT N).f t = (T / S) • (DS N).f (T / S * t)) (uTlim uSlim : C(↑(Set.Icc 0 1), ↥Parabolic.FourierGalerkin.ScalarTorusL2)) (hTlim : Filter.Tendsto (fun (N : ℕ) => classicalGalerkinCoefficientScalarPath N (uT N)) Filter.atTop (nhds uTlim)) (hSlim : Filter.Tendsto (fun (N : ℕ) => classicalGalerkinCoefficientScalarPath N (uS N)) Filter.atTop (nhds uSlim)) (s : ↑(Set.Icc 0 1)) : uTlim s = uSlim ((classicalGalerkinNestedTimeMap T S hT hTS) s)

Increasing-horizon consistency for the exact real-Fourier Galerkin coefficient paths. The finite-path equality is derived from uniqueness of each rescaled coefficient ODE, so only the physical-time scaling identities for its operator and forcing remain as source-specific inputs.

theorem AVenhance.Infra.Classical.classicalGalerkinIncreasingHorizon_consistent (T S : ℝ) (hT : 0 < T) (hTS : T ≤ S) (a b : ℕ → C(↑(Set.Icc 0 1), ↥Parabolic.FourierGalerkin.ScalarTorusL2)) (uT uS : C(↑(Set.Icc 0 1), ↥Parabolic.FourierGalerkin.ScalarTorusL2)) (ha : Filter.Tendsto a Filter.atTop (nhds uT)) (hb : Filter.Tendsto b Filter.atTop (nhds uS)) (hfinite : ∀ (N : ℕ) (s : ↑(Set.Icc 0 1)), (a N) s = (b N) ((classicalGalerkinNestedTimeMap T S hT hTS) s)) (s : ↑(Set.Icc 0 1)) : uT s = uS ((classicalGalerkinNestedTimeMap T S hT hTS) s)

Increasing-horizon consistency follows once the finite Galerkin paths agree after restriction. The limit and approximant types match the word-derivative paths used by the smooth Fourier construction, so this theorem applies separately to every spatial derivative word.