Galerkin Horizon Smoothness Boundary

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Classical.GalerkinHorizonSmoothnessBoundary.classicalBoundaryWordPeriodic (w : List (Fin 2)) (u : Homogenization.Vec 2 → ℝ) (hper : IsZ2Periodic u) : IsZ2Periodic (classicalWordDerivative w u)

theorem AVenhance.Infra.Classical.classicalGalerkinWordPath_hasDerivWithinAt_one (φ : ℝ → 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 ⟨1, ⋯⟩) (Set.Iic 1) 1

The integrated word equation also gives the left time derivative at the terminal edge of the unit slab.

theorem AVenhance.Infra.Classical.classicalGalerkinWordPointwise_hasDerivWithinAt_one (φ : ℝ → 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 1 y + κ * spaceLap (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per ⟨1, ⋯⟩) y - classicalTransport (streamVel φ 1) (classicalGalerkinRealSmoothLift φ hφ κ hκ F hF hFper θ₀ hθ₀ hθ₀per ⟨1, ⋯⟩) y) x) (Set.Iic 1) 1

Pointwise form of the terminal-edge derivative for the real periodic representative.

def AVenhance.Infra.Classical.classicalClosedSlabWordExtension (f q : List (Fin 2) → ℝ × Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) (p : ℝ × Homogenization.Vec 2) : ℝ

Continue a unit-slab solution linearly using its endpoint equation values.

Equations

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

theorem AVenhance.Infra.Classical.classicalClosedSlabWordExtension_hasDerivAt (f q : List (Fin 2) → ℝ × Homogenization.Vec 2 → ℝ) (hinterior : ∀ (w : List (Fin 2)) (x : Homogenization.Vec 2), ∀ t ∈ Set.Ioo 0 1, HasDerivAt (fun (s : ℝ) => f w (s, x)) (q w (t, x)) t) (hzero : ∀ (w : List (Fin 2)) (x : Homogenization.Vec 2), HasDerivWithinAt (fun (s : ℝ) => f w (s, x)) (q w (0, x)) (Set.Ici 0) 0) (hone : ∀ (w : List (Fin 2)) (x : Homogenization.Vec 2), HasDerivWithinAt (fun (s : ℝ) => f w (s, x)) (q w (1, x)) (Set.Iic 1) 1) (w : List (Fin 2)) (x : Homogenization.Vec 2) (t : ℝ) : HasDerivAt (fun (s : ℝ) => classicalClosedSlabWordExtension f q w (s, x)) (q w (↑(classicalGalerkinUnitSlabClamp t), x)) t

Differentiate the endpoint extension along its time slices.

def AVenhance.Infra.Classical.classicalClosedSlabWordExtensionSpaceCoeff (f q : List (Fin 2) → ℝ × Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) (i : Fin 2) (p : ℝ × Homogenization.Vec 2) : ℝ

The spatial coefficient of the derivative of the linearly extended word.

Equations

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

def AVenhance.Infra.Classical.GalerkinHorizonSmoothnessBoundary.classicalClosedSlabWordExtensionSpaceCLM (f q : List (Fin 2) → ℝ × Homogenization.Vec 2 → ℝ) (w : List (Fin 2)) (p : ℝ × Homogenization.Vec 2) : Homogenization.Vec 2 →L[ℝ] ℝ

Spatial differential assembled from the coordinate derivatives of a word extension.

Equations

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

theorem AVenhance.Infra.Classical.classicalSpatialWordFamily_hasFDerivWithinAt (S : Set (ℝ × Homogenization.Vec 2)) (hS : S = Set.Icc 0 1 ×ˢ Set.univ) (f q : List (Fin 2) → ℝ × Homogenization.Vec 2 → ℝ) (hcontinuousF : ∀ (w : List (Fin 2)), Continuous (f w)) (hcontinuousQ : ∀ (w : List (Fin 2)), Continuous (q w)) (hinterior : ∀ (w : List (Fin 2)) (x : Homogenization.Vec 2), ∀ t ∈ Set.Ioo 0 1, HasDerivAt (fun (s : ℝ) => f w (s, x)) (q w (t, x)) t) (hzero : ∀ (w : List (Fin 2)) (x : Homogenization.Vec 2), HasDerivWithinAt (fun (s : ℝ) => f w (s, x)) (q w (0, x)) (Set.Ici 0) 0) (hone : ∀ (w : List (Fin 2)) (x : Homogenization.Vec 2), HasDerivWithinAt (fun (s : ℝ) => f w (s, x)) (q w (1, x)) (Set.Iic 1) 1) (hspaceF : ∀ (w : List (Fin 2)) (t : ℝ) (x : Homogenization.Vec 2), HasFDerivAt (fun (y : Homogenization.Vec 2) => f w (t, y)) (∑ i : Fin 2, f (i :: w) (t, x) • ContinuousLinearMap.proj i) x) (hspaceQ : ∀ (w : List (Fin 2)) (t : ℝ) (x : Homogenization.Vec 2), HasFDerivAt (fun (y : Homogenization.Vec 2) => q w (t, y)) (∑ i : Fin 2, q (i :: w) (t, x) • ContinuousLinearMap.proj i) x) (w : List (Fin 2)) (p : ℝ × Homogenization.Vec 2) : p ∈ S → HasFDerivWithinAt (f w) (classicalSpatialWordDerivativeLinearMap f q w p) S p

Assemble the equation derivative and all coordinate derivatives into the full derivative within the closed unit slab.