Coarse-graining support: Support.HighContrast.EntryScale.DeterministicAlgebra.P4

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.HighContrast.EntryScale.tau_mul_response_le_sqrt_budget_sq_of_rtau_response_bounds {tau response r_m C_response C_sqrt rho delta F_m : ℝ} (hr_pos : 0 < r_m) (hresponse_nonneg : 0 ≤ response) (hrho_nonneg : 0 ≤ rho) (hdelta_pos : 0 < delta) (hdelta_le_F : delta ≤ F_m) (hrt : r_m * tau ≤ 1 / 2 * (rho * F_m)) (hresponse : response ≤ C_response * r_m) (hC_response_nonneg : 0 ≤ C_response) (hC_response_le : C_response ≤ C_sqrt ^ 2) : tau * response ≤ (C_sqrt * √rho * √delta⁻¹ * F_m) ^ 2

Source label e.sqrt.tau.absorb: product estimate obtained from the terminal tau-drop bound and the linear lower-scale response expectation bound used in the note.

theorem HCPolySupport.HighContrast.EntryScale.drift_general_square_bound {D C rho F_m T_m : ℝ} (hD_nonneg : 0 ≤ D) (hC_nonneg : 0 ≤ C) (hrho_nonneg : 0 ≤ rho) (hF_pos : 0 < F_m) (hT : T_m = (1 + F_m) ^ 2 / F_m) (hD : D ≤ C * (rho * F_m) / (1 + F_m)) : D ^ 2 ≤ C ^ 2 * rho ^ 2 * F_m / T_m

Source labels e.drift.general and e.drift.nodrop: the pointwise square bound behind the weighted no-drop drift estimate when T_m = (1 + F_m)^2 / F_m.

theorem HCPolySupport.HighContrast.EntryScale.terminal_weight_le_delta_mul {T_m F_m delta : ℝ} (hdelta_pos : 0 < delta) (hdelta_le_F : delta ≤ F_m) (hT : T_m = (1 + F_m) ^ 2 / F_m) : T_m ≤ (1 + delta⁻¹) ^ 2 * F_m

Source label l.S.and.J, equation e.S.term.bound: above the small-contrast threshold, the terminal weight T_m = (1 + F_m)^2 / F_m is bounded by a threshold-dependent multiple of F_m.

theorem HCPolySupport.HighContrast.EntryScale.terminal_weight_le_const_mul {T_m F_m delta C_delta : ℝ} (hdelta_pos : 0 < delta) (hdelta_le_F : delta ≤ F_m) (hT : T_m = (1 + F_m) ^ 2 / F_m) (hC_delta : (1 + delta⁻¹) ^ 2 ≤ C_delta) : T_m ≤ C_delta * F_m

Source label l.S.and.J, equation e.S.term.bound: constant-form version of the small-contrast threshold absorption used for the paper's C_{\delta_{\rm sc}}.

theorem HCPolySupport.HighContrast.EntryScale.terminal_weight_mul_term_le_const_mul_contrast_of_le {T_m F_m delta C_delta term eta : ℝ} (hdelta_pos : 0 < delta) (hdelta_le_F : delta ≤ F_m) (hT : T_m = (1 + F_m) ^ 2 / F_m) (hC_delta : (1 + delta⁻¹) ^ 2 ≤ C_delta) (hterm_nonneg : 0 ≤ term) (hterm_le : term ≤ eta) : T_m * term ≤ C_delta * eta * F_m

Source label l.S.and.J, equation e.S.term.bound: after the terminal fluctuation sum is made small, the small-contrast threshold converts T_m S_{k,m} into a multiple of F_m.

theorem HCPolySupport.HighContrast.EntryScale.one_add_contrast_le_terminal_weight {T_m F_m : ℝ} (hF_pos : 0 < F_m) (hT : T_m = (1 + F_m) ^ 2 / F_m) : 1 + F_m ≤ T_m

Source label l.S.and.J, equation e.J.moment.bound: the terminal weight dominates the terminal contrast scale 1 + F_m = r_m^2.

theorem HCPolySupport.HighContrast.EntryScale.cutoff_contrast_geo_le_decay_terminal_weight {A geom F_m decay T_m : ℝ} (hA_nonneg : 0 ≤ A) (hcoeff : A * geom ≤ decay) (hgeom_nonneg : 0 ≤ geom) (hF_pos : 0 < F_m) (hT : T_m = (1 + F_m) ^ 2 / F_m) : A * (geom * F_m) ≤ decay * T_m

Source label p.HC.CR: scalar absorption for the raw cutoff geometric tail. Once the two-beta coefficient has been made at most decay, the terminal weight pays the remaining contrast factor.

theorem HCPolySupport.HighContrast.EntryScale.weighted_drift_square_bound {ι : Type u_1} (s : Finset ι) {w D : ι → ℝ} {T_m C Cw rho F_m : ℝ} (hT_pos : 0 < T_m) (hC_nonneg : 0 ≤ C) (hF_nonneg : 0 ≤ F_m) (hw_nonneg : ∀ i ∈ s, 0 ≤ w i) (hDsq : ∀ i ∈ s, D i ^ 2 ≤ C * rho ^ 2 * F_m / T_m) (hCw : ∑ i ∈ s, w i ≤ Cw) : T_m * ∑ i ∈ s, w i * D i ^ 2 ≤ C * Cw * rho ^ 2 * F_m

Source label e.drift.nodrop: finite weighted-square form of the deterministic drift estimate on a no-drop window.