Continuous right-hand-side paths for every ordered spatial derivative of the limit equation.
@[instance_reducible]
Use normalized Haar measure on the unit circle for periodic integrals.
Equations
- classicalWordEquationMeasureSpace = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }
Instances For
theorem
AVenhance.Infra.Classical.GalerkinSmoothWordEquation.classicalSmoothWordPeriodic
(w : List (Fin 2))
(f : Homogenization.Vec 2 → ℝ)
(hper : IsZ2Periodic f)
:
theorem
AVenhance.Infra.Classical.GalerkinSmoothWordEquation.classicalWordDerivative_append
(v w : List (Fin 2))
(f : Homogenization.Vec 2 → ℝ)
:
theorem
AVenhance.Infra.Classical.GalerkinSmoothWordEquation.classicalWordDerivative_add
(w : List (Fin 2))
(f g : Homogenization.Vec 2 → ℝ)
(hf : ContDiff ℝ (↑⊤) f)
(hg : ContDiff ℝ (↑⊤) g)
:
(classicalWordDerivative w fun (x : Homogenization.Vec 2) => f x + g x) = fun (x : Homogenization.Vec 2) =>
classicalWordDerivative w f x + classicalWordDerivative w g x
theorem
AVenhance.Infra.Classical.GalerkinSmoothWordEquation.classicalSpaceLap_contDiff_word
(f : Homogenization.Vec 2 → ℝ)
(hf : ContDiff ℝ (↑⊤) f)
:
ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => spaceLap f x
theorem
AVenhance.Infra.Classical.GalerkinSmoothWordEquation.classicalTransport_contDiff_word
(b : Homogenization.Vec 2 → Homogenization.Vec 2)
(u : Homogenization.Vec 2 → ℝ)
(hb : ContDiff ℝ (↑⊤) b)
(hu : ContDiff ℝ (↑⊤) u)
:
ContDiff ℝ (↑⊤) (classicalTransport b u)
noncomputable def
AVenhance.Infra.Classical.classicalSmoothWordJointPath
(g : ℝ × Homogenization.Vec 2 → ℝ)
(hg : ContDiffOn ℝ (↑⊤) g classicalHalfSpace)
(hper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic fun (x : Homogenization.Vec 2) => g (t, x))
(w : List (Fin 2))
:
Descend the spatial derivative of a jointly smooth, spatially periodic scalar family.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AVenhance.Infra.Classical.classicalSmoothWordJointPath_apply
(g : ℝ × Homogenization.Vec 2 → ℝ)
(hg : ContDiffOn ℝ (↑⊤) g classicalHalfSpace)
(hper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic fun (x : Homogenization.Vec 2) => g (t, x))
(w : List (Fin 2))
(t : ↑(Set.Icc 0 1))
(x : UnitAddTorus (Fin 2))
:
(classicalSmoothWordJointPath g hg hper w) (t, x) = ↑(classicalWordDerivative w (fun (y : Homogenization.Vec 2) => g (↑t, y)) (Torus.unitTorusRepresentative 2 x))
noncomputable def
AVenhance.Infra.Classical.classicalGalerkinForcingWordJointPath
(F : ℝ → Homogenization.Vec 2 → ℝ)
(hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) (Set.Ici 0 ×ˢ Set.univ))
(hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t))
(w : List (Fin 2))
:
The forcing after an arbitrary ordered spatial derivative, on the time-space torus slab.
Equations
Instances For
noncomputable def
AVenhance.Infra.Classical.classicalGalerkinDriftWordJointPath
(φ : ℝ → Homogenization.Vec 2 → ℝ)
(hφ : IsAdmissibleStream φ)
(w : List (Fin 2))
(j : Fin 2)
:
A spatial derivative of a drift coordinate, descended to the time-space torus slab.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AVenhance.Infra.Classical.classicalGalerkinDriftWordJointPath_apply
(φ : ℝ → Homogenization.Vec 2 → ℝ)
(hφ : IsAdmissibleStream φ)
(w : List (Fin 2))
(j : Fin 2)
(t : ↑(Set.Icc 0 1))
(x : UnitAddTorus (Fin 2))
:
(classicalGalerkinDriftWordJointPath φ hφ w j) (t, x) = ↑(classicalWordDerivative w (fun (y : Homogenization.Vec 2) => streamVel φ (↑t) y j)
(Torus.unitTorusRepresentative 2 x))
noncomputable def
AVenhance.Infra.Classical.classicalGalerkinSmoothWordRhsJointPath
(φ : ℝ → 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))
:
All spatial derivatives of the limiting physical right-hand side, represented continuously on the closed unit time slab and the spatial torus.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
AVenhance.Infra.Classical.classicalGalerkinSmoothWordRhsJointPath_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 θ₀)
(w : List (Fin 2))
(t : ↑(Set.Icc 0 1))
(x : UnitAddTorus (Fin 2))
:
(classicalGalerkinSmoothWordRhsJointPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w) (t, x) = ↑(classicalWordDerivative w
(fun (y : Homogenization.Vec 2) =>
F (↑t) y + κ * spaceLap (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t) y - classicalTransport (streamVel φ ↑t) (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t) y)
(Torus.unitTorusRepresentative 2 x))
theorem
AVenhance.Infra.Classical.GalerkinSmoothWordEquation.classicalSmoothWordFourierCoeff_multiplier
(f : Homogenization.Vec 2 → ℝ)
(hf : ContDiff ℝ (↑⊤) f)
(hper : IsZ2Periodic f)
(w : List (Fin 2))
(k : Fin 2 → ℤ)
:
theorem
AVenhance.Infra.Classical.classicalGalerkinSmoothWordRhsJointPath_fourierCoeff
(φ : ℝ → 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 (⇑((classicalGalerkinSmoothWordRhsJointPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w).curry t))
k = classicalGalerkinWordFourierMultiplier k w * UnitAddTorus.mFourierCoeff (⇑((classicalGalerkinSmoothRhsJointPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per).curry t)) k
theorem
AVenhance.Infra.Classical.classicalGalerkinWordPath_integral_eq
(φ : ℝ → 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))
:
(classicalGalerkinWordFourierContinuousPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w).curry t = (classicalGalerkinWordFourierContinuousPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w).curry 0 + ∫ (s : ℝ) in 0..↑t, (classicalGalerkinSmoothWordRhsJointPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w).curry
(classicalGalerkinUnitSlabClamp s)
Each spatial derivative path satisfies the limiting equation in time-integrated form.
theorem
AVenhance.Infra.Classical.classicalGalerkinWordPath_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))
{t : ℝ}
(ht : t ∈ Set.Ioo 0 1)
:
HasDerivAt
(fun (s : ℝ) =>
(classicalGalerkinWordFourierContinuousPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w).curry
(classicalGalerkinUnitSlabClamp s))
((classicalGalerkinSmoothWordRhsJointPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w).curry ⟨t, ⋯⟩) t
Interior time differentiability of every spatial word, with derivative given by its continuous right-hand-side path.
theorem
AVenhance.Infra.Classical.classicalGalerkinWordLift_jointContinuous
(φ : ℝ → 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))
:
Continuous fun (p : ↑(Set.Icc 0 1) × Homogenization.Vec 2) =>
classicalWordDerivative w (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per p.1) p.2
Every spatial word of the smooth Galerkin lift is jointly continuous on the closed unit slab.
theorem
AVenhance.Infra.Classical.classicalGalerkinWordPointwise_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))
(x : Homogenization.Vec 2)
{t : ℝ}
(ht : t ∈ Set.Ioo 0 1)
:
HasDerivAt
(fun (s : ℝ) =>
classicalWordDerivative w
(classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per (classicalGalerkinUnitSlabClamp s)) x)
(classicalWordDerivative w
(fun (y : Homogenization.Vec 2) =>
F t y + κ * spaceLap (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per ⟨t, ⋯⟩) y - classicalTransport (streamVel φ t) (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per ⟨t, ⋯⟩)
y)
x)
t
Pointwise interior time differentiability of every spatial derivative of the smooth lift.
theorem
AVenhance.Infra.Classical.classicalGalerkinWordPath_hasDerivWithinAt_zero
(φ : ℝ → 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))
:
HasDerivWithinAt
(fun (s : ℝ) =>
(classicalGalerkinWordFourierContinuousPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w).curry
(classicalGalerkinUnitSlabClamp s))
((classicalGalerkinSmoothWordRhsJointPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w).curry ⟨0, ⋯⟩) (Set.Ici 0) 0
Right time differentiability at the initial boundary for every spatial word, as a torus-valued path.
theorem
AVenhance.Infra.Classical.classicalGalerkinWordPointwise_hasDerivWithinAt_zero
(φ : ℝ → 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))
(x : Homogenization.Vec 2)
:
HasDerivWithinAt
(fun (s : ℝ) =>
classicalWordDerivative w
(classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per (classicalGalerkinUnitSlabClamp s)) x)
(classicalWordDerivative w
(fun (y : Homogenization.Vec 2) =>
F 0 y + κ * spaceLap (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per ⟨0, ⋯⟩) y - classicalTransport (streamVel φ 0) (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per ⟨0, ⋯⟩)
y)
x)
(Set.Ici 0) 0
Pointwise right time differentiability at the initial boundary, with the derivative given by the physical right-hand side.
theorem
AVenhance.Infra.Classical.classicalGalerkinSmoothWordRhsJointPath_apply_toEuclidean
(φ : ℝ → 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))
(x : Homogenization.Vec 2)
:
(classicalGalerkinSmoothWordRhsJointPath φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per w) (t, Torus.toUnitTorus 2 x) = ↑(classicalWordDerivative w
(fun (y : Homogenization.Vec 2) =>
F (↑t) y + κ * spaceLap (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t) y - classicalTransport (streamVel φ ↑t) (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per t) y)
x)
The torus right-hand-side path agrees with the Euclidean periodic formula at every spatial point, including the canonical representative boundary.