Coarse-to-fine rate conversion for actual lower gradient levels.

theorem AVenhance.Infra.Section4.amnr_gradient_material_spatial_scale {E β : ℝ} (hE : 0 < E) (k r : ℕ) : E ^ (β - 2) * E⁻¹ ^ k * (E ^ (β - 2)) ^ r = E ^ ((β - 2) * (↑r + 1) - ↑k)

theorem AVenhance.Infra.Section4.amnr_gradient_material_scale_antitone {E F β : ℝ} (hE : 0 < E) (hF : 0 < F) (hEF : E ≤ F) (hβ : β < 4 / 3) (k r : ℕ) : F ^ (β - 2) * F⁻¹ ^ k * (F ^ (β - 2)) ^ r ≤ E ^ (β - 2) * E⁻¹ ^ k * (E ^ (β - 2)) ^ r

theorem AVenhance.Infra.Section4.amnr_epsilon_current_le_prev {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) : epsilon β I.Λ m ≤ epsilon β I.Λ (m - 1)