Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section4.Amnr.TemperatureCoefficientTopSourceBounds

Literal source coefficients through the terminal permitted scale.

source
noncomputable def AVenhance.Infra.Section4.amnrSourceRatioConstant (β C : ℝ) :
ℝ

Constant controlling the diffusivity ratio in the source estimate.

Equations
Instances For
    source
    theorem AVenhance.Infra.Section4.amnrSourceRatioConstant_nonneg {β C : ℝ} (I : Ingredients β) (hC : 0 ≤ C) :
    0 ≤ amnrSourceRatioConstant β C