Statement file: IsWeakSolution (Roots).
This file contains exactly one declaration of the formalization's public statement surface.
def
AVenhance.IsWeakSolution
(b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2)
(κ : ℝ)
(θ₀ : Homogenization.Vec 2 → ℝ)
(θ : ℝ → Homogenization.Vec 2 → ℝ)
:
θ is a weak solution of the advection–diffusion equation with drift b, diffusivity κ and
initial datum θ₀, for some spatial weak gradient Dθ.
Equations
- AVenhance.IsWeakSolution b κ θ₀ θ = ∃ (Dθ : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2), AVenhance.IsWeakSolutionGrad b κ θ₀ θ Dθ