Differentiated energies of a classical solution #
For an ordered derivative word w, the energy ‖∂^w θ(s)‖² of a classical solution is continuous
on
[0,T] and has the derivative -2κ ‖∇∂^w θ‖² - 2 C_w(s) at every s > 0, where
C_w(s) = ∫ ∂^wθ (∂^w(b·∇θ) - b·∇∂^wθ) is the commutator pairing. The gradient dissipation is
continuous on [0,∞).
noncomputable def
AVenhance.Infra.FullTheorem.Separation.wEnergy
(w : List (Fin 2))
(θ : ℝ → Homogenization.Vec 2 → ℝ)
(s : ℝ)
:
‖∂^w θ(s)‖²_{L²(cell)}.
Equations
Instances For
noncomputable def
AVenhance.Infra.FullTheorem.Separation.wDiss
(w : List (Fin 2))
(θ : ℝ → Homogenization.Vec 2 → ℝ)
(s : ℝ)
:
‖∇∂^w θ(s)‖²_{L²(cell)}.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
AVenhance.Infra.FullTheorem.Separation.wComm
(w : List (Fin 2))
(Ψ θ : ℝ → Homogenization.Vec 2 → ℝ)
(s : ℝ)
:
The commutator pairing ∫ ∂^wθ (∂^w(b·∇θ) - b·∇∂^wθ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Joint time-space domain with nonnegative time, including the initial trace.
Instances For
theorem
AVenhance.Infra.FullTheorem.Separation.wEnergy_continuousOn
{θ : ℝ → Homogenization.Vec 2 → ℝ}
(hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) (Set.Ici 0 ×ˢ Set.univ))
(w : List (Fin 2))
{T : ℝ}
(hT : 0 ≤ T)
:
ContinuousOn (wEnergy w θ) (Set.Icc 0 T)
theorem
AVenhance.Infra.FullTheorem.Separation.wDiss_continuousOn
{θ : ℝ → Homogenization.Vec 2 → ℝ}
(hθ : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) (Set.Ici 0 ×ˢ Set.univ))
(w : List (Fin 2))
:
ContinuousOn (wDiss w θ) (Set.Ici 0)
theorem
AVenhance.Infra.FullTheorem.Separation.wEnergy_hasDerivAt
{Ψ θ : ℝ → Homogenization.Vec 2 → ℝ}
{κ : ℝ}
{θ₀ : Homogenization.Vec 2 → ℝ}
(hΨ : IsAdmissibleStream Ψ)
(hsol : IsClassicalSol (streamVel Ψ) κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θ)
(w : List (Fin 2))
{t : ℝ}
(ht : 0 < t)
: