Finite Galerkin time-change identities for nested physical horizons.

@[instance_reducible]

noncomputable def galerkinHorizonConsistencyMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem galerkinHorizonConsistencyMeasureIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem galerkinHorizonConsistencyProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem galerkinHorizonConsistencyProbabilityTorus : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

noncomputable def AVenhance.Infra.Classical.GalerkinHorizonConsistency.classicalGalerkinGeneratorCLM (φ : ℝ → Homogenization.Vec 2 → ℝ) (κ : ℝ) (K : ℕ) (t : ℝ) : Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension K) →L[ℝ] Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension K)

Continuous linear Galerkin generator at a given time and frequency cutoff.

Equations

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

theorem AVenhance.Infra.Classical.GalerkinHorizonConsistency.classicalGalerkinWeakEntry_horizon_eq (H K : ℕ) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ s : ℝ) (i j : Fin (Parabolic.FourierGalerkin.RealFourierDimension K)) : Parabolic.FourierGalerkin.weakFormMatrixEntry (fun (r : ℝ) (x : Parabolic.FourierGalerkin.Torus) => Torus.periodicToTorus (streamVel (classicalGalerkinHorizonStream H φ) r) x) (↑H * κ) (Parabolic.FourierGalerkin.realFourierModeFin K) (Parabolic.FourierGalerkin.realFourierModeGradFin K) s i j = ↑H * Parabolic.FourierGalerkin.weakFormMatrixEntry (fun (r : ℝ) (x : Parabolic.FourierGalerkin.Torus) => Torus.periodicToTorus (streamVel φ r) x) κ (Parabolic.FourierGalerkin.realFourierModeFin K) (Parabolic.FourierGalerkin.realFourierModeGradFin K) (↑H * s) i j

theorem AVenhance.Infra.Classical.GalerkinHorizonConsistency.classicalGalerkinGeneratorCLM_horizon_eq (H K : ℕ) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ s : ℝ) : classicalGalerkinGeneratorCLM (classicalGalerkinHorizonStream H φ) (↑H * κ) K s = ↑H • classicalGalerkinGeneratorCLM φ κ K (↑H * s)

theorem AVenhance.Infra.Classical.classicalForcingCoefficients_horizon_eq (H K : ℕ) (F : ℝ → Homogenization.Vec 2 → ℝ) {s : ℝ} (hs : 0 ≤ s) : classicalForcingCoefficients K (classicalGalerkinHorizonForcing H F) s = ↑H • classicalForcingCoefficients K F (↑H * s)

noncomputable def AVenhance.Infra.Classical.classicalGalerkinHorizonODEData (H : ℕ) (hH : 0 < H) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (K : ℕ) : ODE.LinearODEData 0 1 classicalGalerkinHorizonODEData._proof_1

The finite ODE data obtained by running the Galerkin construction on a physical integer horizon.

Equations

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

theorem AVenhance.Infra.Classical.GalerkinHorizonConsistency.classicalGalerkinHorizonODEData_A_eq_generator (H : ℕ) (hH : 0 < H) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (K : ℕ) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : (classicalGalerkinHorizonODEData H hH φ hφ κ hκ F hF θ₀ hθ₀ K).A t = classicalGalerkinGeneratorCLM (classicalGalerkinHorizonStream H φ) (↑H * κ) K t

theorem AVenhance.Infra.Classical.GalerkinHorizonConsistency.classicalGalerkinHorizonODEData_f_eq_forcing (H : ℕ) (hH : 0 < H) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (K : ℕ) (t : ℝ) : (classicalGalerkinHorizonODEData H hH φ hφ κ hκ F hF θ₀ hθ₀ K).f t = classicalForcingCoefficients K (classicalGalerkinHorizonForcing H F) t

theorem AVenhance.Infra.Classical.classicalGalerkinHorizonOperator_rescale (T S K : ℕ) (hT : 0 < T) (hTS : T ≤ S) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : (classicalGalerkinHorizonODEData T hT φ hφ κ hκ F hF θ₀ hθ₀ K).A t = (↑T / ↑S) • (classicalGalerkinHorizonODEData S ⋯ φ hφ κ hκ F hF θ₀ hθ₀ K).A (↑T / ↑S * t)

The horizon-rescaled weak operators satisfy the hA identity required by finite-path uniqueness on nested horizons.

theorem AVenhance.Infra.Classical.classicalGalerkinHorizonForcing_rescale (T S K : ℕ) (hT : 0 < T) (hTS : T ≤ S) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : (classicalGalerkinHorizonODEData T hT φ hφ κ hκ F hF θ₀ hθ₀ K).f t = (↑T / ↑S) • (classicalGalerkinHorizonODEData S ⋯ φ hφ κ hκ F hF θ₀ hθ₀ K).f (↑T / ↑S * t)

The horizon-rescaled forcing vectors satisfy the hf identity required by finite-path uniqueness on nested horizons.

theorem AVenhance.Infra.Classical.GalerkinHorizonConsistency.classicalGalerkinHorizonODEData_y₀_eq_projection (H : ℕ) (hH : 0 < H) (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (κ : ℝ) (hκ : 0 < κ) (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ)) (θ₀ : Homogenization.Vec 2 → ℝ) (hθ₀ : ContDiff ℝ (↑⊤) θ₀) (K : ℕ) : (classicalGalerkinHorizonODEData H hH φ hφ κ hκ F hF θ₀ hθ₀ K).y₀ = Parabolic.FourierGalerkin.modeProjectionCoefficients (Parabolic.FourierGalerkin.RealFourierDimension K) (Parabolic.FourierGalerkin.realFourierModeFin K) (Torus.periodicToTorus θ₀)

theorem AVenhance.Infra.Classical.classicalGalerkinHorizonLimitL2_consistent (T S : ℕ) (hT : 0 < T) (hTS : T ≤ S) (φ : ℝ → 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 θ₀) (s : ↑(Set.Icc 0 1)) : (classicalGalerkinWordScalarPathLimit (classicalGalerkinHorizonStream T φ) ⋯ (↑T * κ) ⋯ (classicalGalerkinHorizonForcing T F) ⋯ ⋯ θ₀ hθ₀ hθ₀per []) s = (classicalGalerkinWordScalarPathLimit (classicalGalerkinHorizonStream S φ) ⋯ (↑S * κ) ⋯ (classicalGalerkinHorizonForcing S F) ⋯ ⋯ θ₀ hθ₀ hθ₀per []) ((classicalGalerkinNestedTimeMap ↑T ↑S ⋯ ⋯) s)

The base L² Galerkin limits on nested integer horizons agree under physical-time restriction. This is the sequence-level consistency needed to patch the smooth representatives.

theorem AVenhance.Infra.Classical.GalerkinHorizonConsistency.classicalRealToComplexTorusCLM_injective : Function.Injective ⇑classicalRealToComplexTorusCLM

theorem AVenhance.Infra.Classical.GalerkinHorizonConsistency.classicalPeriodicRealFunctions_eq_of_L2_eq (u v : Homogenization.Vec 2 → ℝ) (hu : Continuous u) (hv : Continuous v) (hup : IsZ2Periodic u) (hvp : IsZ2Periodic v) (hL2 : MeasureTheory.MemLp.toLp (Torus.periodicToTorus u) ⋯ = MeasureTheory.MemLp.toLp (Torus.periodicToTorus v) ⋯) : u = v

@[irreducible]

noncomputable def AVenhance.Infra.Classical.classicalGalerkinHorizonSmoothSlice (H : ℕ) (hH : 0 < H) (φ : ℝ → 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 θ₀) (s : ↑(Set.Icc 0 1)) : Homogenization.Vec 2 → ℝ

The smooth unit-slab representative associated with a positive physical integer horizon.

Equations

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

theorem AVenhance.Infra.Classical.classicalGalerkinHorizonSmoothLimit_consistent (T S : ℕ) (hT : 0 < T) (hTS : T ≤ S) (φ : ℝ → 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 θ₀) (s : ↑(Set.Icc 0 1)) : classicalGalerkinHorizonSmoothSlice T hT φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per s = classicalGalerkinHorizonSmoothSlice S ⋯ φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per ((classicalGalerkinNestedTimeMap ↑T ↑S ⋯ ⋯) s)

The smooth unit-slab representatives themselves agree on nested integer horizons.

theorem AVenhance.Infra.Classical.classicalGalerkinHorizonLimit_consistent_on_overlap (T S : ℕ) (hT : 0 < T) (hTS : T ≤ S) (φ : ℝ → 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 : ℝ} (ht : t ∈ Set.Icc 0 ↑T) : classicalGalerkinHorizonLimit T hT φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t = classicalGalerkinHorizonLimit S ⋯ φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t

Physical-time smooth limits from a shorter integer horizon agree pointwise with those from a longer horizon throughout the shorter closed interval.

@[irreducible]

noncomputable def AVenhance.Infra.Classical.classicalGalerkinIntegerHorizonFamily (φ : ℝ → 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 θ₀) : ℕ → ℝ → Homogenization.Vec 2 → ℝ

Use horizon N+1 at family index N, so every member has a positive horizon.

Equations

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

theorem AVenhance.Infra.Classical.classicalGalerkinIntegerHorizonFamily_periodic (φ : ℝ → 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 θ₀) (N : ℕ) (t : ℝ) : 0 ≤ t → IsZ2Periodic (classicalGalerkinIntegerHorizonFamily φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per N t)

theorem AVenhance.Infra.Classical.classicalGalerkinIntegerHorizonFamily_initial (φ : ℝ → 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 θ₀) (N : ℕ) (x : Homogenization.Vec 2) : classicalGalerkinIntegerHorizonFamily φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per N 0 x = θ₀ x

theorem AVenhance.Infra.Classical.classicalGalerkinIntegerHorizonFamily_advDiffOp (φ : ℝ → 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 θ₀) (n : ℕ) (t : ℝ) : t ∈ Set.Ioo 0 ↑n.succ → ∀ (x : Homogenization.Vec 2), advDiffOp (streamVel φ) κ (classicalGalerkinIntegerHorizonFamily φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per n) t x = F t x

theorem AVenhance.Infra.Classical.classicalGalerkinIntegerHorizonFamily_consistent (φ : ℝ → 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 θ₀) (M N : ℕ) : M ≤ N → ∀ t ∈ Set.Icc 0 ↑M, classicalGalerkinIntegerHorizonFamily φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per M t = classicalGalerkinIntegerHorizonFamily φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per N t