Composed analyticity of the slow factors: assembly

Feeds the word bounds of Q, A, Y' (TermCenteredAnalyticJets), the temperature jets and the flow jets (TermCenteredAnalyticInputs) and smoothness/periodicity (TermCenteredAnalyticSmooth) to slowFactorChoice2/3_composed_bounds, and weakens the resulting radius and amplitude to the normalised ones ρ / c₂, c₁ κ S ρ⁻².

theorem AVenhance.Infra.Section5.Contracts.sdc_hasCoordinate_mono {f : Homogenization.Vec 2 → ℂ} {Cf Cf' r r' : ℝ} (h : Ergodic.HasCoordinateAnalyticL2Bounds f Cf r) (hCf : 0 ≤ Cf) (hC : Cf ≤ Cf') (hr' : 0 < r') (hr : r' ≤ r) : Ergodic.HasCoordinateAnalyticL2Bounds f Cf' r'

HasCoordinateAnalyticL2Bounds is monotone in the amplitude and anti-monotone in the radius.

theorem AVenhance.Infra.Section5.Contracts.sdc_radius_ge {ε ρ K A₁ : ℝ} (hρ : 0 < ρ) (hρε : ρ ≤ ε) (hK : 1 ≤ K) (hA₁ : 1 ≤ A₁) : ρ / (2 * 2 ^ 14 * 33 * K * A₁) ≤ (16 * (A₁ / ρ))⁻¹ / (2 * 2 ^ 14 / ε * ((16 * (A₁ / ρ))⁻¹ + 2 * (K * ε)))

Abstract-real radius arithmetic.