Monotonicity of the jet inputs and real-variable scale facts

theorem AVenhance.Infra.Section5.Contracts.sd_jets_mono {A A' ρ S : ℝ} {T : ℝ → Homogenization.Vec 2 → ℝ} (hA : 0 ≤ A) (hAA : A ≤ A') (hρ : 0 < ρ) (hS : 0 ≤ S) (h : RelativeError.PositiveTemperatureJets A ρ S T) : RelativeError.PositiveTemperatureJets A' ρ S T

The positive-jet hypothesis is monotone in the constant.

theorem AVenhance.Infra.Section5.Contracts.sd_rN_facts {x y K c₂ q g δ : ℝ} (hx : 0 < x) (hx1 : x ≤ 1) (hy : 0 < y) (hyK : y ≤ K * x ^ q) (hK : 1 ≤ K) (hc₂ : 0 < c₂) (hexp : 2 * δ ≤ q - 1 - g / 2) (hsmall : x ^ (2 * δ) ≤ 1 / (2 * c₂ * K)) : 1 / (4096 * c₂ * K) * x ^ (-(2 * δ)) ≤ x ^ (1 + g / 2) / c₂ * y⁻¹ / 4096 ∧ 2 ≤ x ^ (1 + g / 2) / c₂ * y⁻¹

Real-variable lower bound of the exponential argument r N / 4096, with r = x^{1+g/2}/c₂, N = y⁻¹, y ≤ K x^q, 2δ ≤ q - 1 - g/2.