Elementary positivity and monotonicity facts for the diffusivity chain.

theorem AVenhance.Infra.Section3.khomScalar_ge_input {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) : κ ≤ I.KhomScalar κ m

The averaged scalar diffusivity is at least the molecular diffusivity.

theorem AVenhance.Infra.Section3.khomScalar_le_input_add_amplitude {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) : I.KhomScalar κ m ≤ κ + a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / (2 * κ)

The averaged scalar diffusivity also has the upper bound inherited from the pointwise memory relaxation estimate.

theorem AVenhance.Infra.Section3.kappaAt_pos {β : ℝ} (I : Ingredients β) {κ : ℝ} (hκ : 0 < κ) (m d : ℕ) : 0 < I.kappaAt κ m d

Every value in the recurrence is positive when its terminal value is.