Statement file: IsWeakSolutionGrad (Roots).
This file contains exactly one declaration of the formalization's public statement surface.
def
AVenhance.IsWeakSolutionGrad
(b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2)
(κ : ℝ)
(θ₀ : Homogenization.Vec 2 → ℝ)
(θ : ℝ → Homogenization.Vec 2 → ℝ)
(Dθ : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2)
:
The weak-solution notion with the gradient Dθ explicit: weak solution on [0,1] × 𝕋² of
∂ₜθ + b·∇θ − κΔθ = 0, θ(0) = θ₀. The drift term is required to be
integrable on the space-time cell, so no integral in the weak form can take the
Bochner junk value.
Equations
- One or more equations did not get rendered due to their size.