Coarse-graining support: Support.Book.Ch05.Theorems.Section54.GoodScale.SpecialVectorAlgebra

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

Special-vector scalar algebra for the good-scale lemma

This file contains only the real-variable algebra behind the manuscript choices p_e = \widehat\sigma_m^{-1/2} e and q_e = \widehat\sigma_m^{1/2} e. The law-facing good-scale theorem will use these identities after the manuscript-facing scalar hypotheses are available.

theorem HCPolySupport.Book.Ch05.Section54.GoodScale.sigma_mul_inv_star_eq_sqrt_theta {b c sigma theta : ℝ} (hb : 0 < b) (hc : 0 < c) (hsigma : sigma = √(b * c)) (htheta : theta = b * c⁻¹) : sigma * c⁻¹ = √theta

With σ = sqrt (b * c) and θ = b * c⁻¹, the product σ * c⁻¹ is sqrt θ.

theorem HCPolySupport.Book.Ch05.Section54.GoodScale.barSigma_mul_inv_sigma_eq_sqrt_theta {b c sigma theta : ℝ} (hb : 0 < b) (hc : 0 < c) (hsigma : sigma = √(b * c)) (htheta : theta = b * c⁻¹) : b * sigma⁻¹ = √theta

With σ = sqrt (b * c) and θ = b * c⁻¹, the product b * σ⁻¹ is sqrt θ.

theorem HCPolySupport.Book.Ch05.Section54.GoodScale.rpow_neg_half_mul_rpow_half_eq_one {sigma : ℝ} (hsigma_pos : 0 < sigma) : sigma ^ (-(1 / 2)) * sigma ^ (1 / 2) = 1

The product of the negative and positive half-powers of a positive scalar.

theorem HCPolySupport.Book.Ch05.Section54.GoodScale.rpow_half_sq_eq_self {sigma : ℝ} (hsigma_pos : 0 < sigma) : (sigma ^ (1 / 2)) ^ 2 = sigma

The square of the positive half-power of a positive scalar.

theorem HCPolySupport.Book.Ch05.Section54.GoodScale.rpow_neg_half_sq_eq_inv {sigma : ℝ} (hsigma_pos : 0 < sigma) : (sigma ^ (-(1 / 2))) ^ 2 = sigma⁻¹

The square of the negative half-power of a positive scalar.

theorem HCPolySupport.Book.Ch05.Section54.GoodScale.rpow_half_mul_specialP_centering_coeff_eq {b c sigma theta : ℝ} (hb : 0 < b) (hc : 0 < c) (hsigma : sigma = √(b * c)) (htheta : theta = b * c⁻¹) : sigma ^ (1 / 2) * (c⁻¹ * sigma ^ (1 / 2) - sigma ^ (-(1 / 2))) = √theta - 1

Coefficient identity for the scaled centered special vector p_e.

theorem HCPolySupport.Book.Ch05.Section54.GoodScale.rpow_neg_half_mul_specialQ_centering_coeff_eq {b c sigma theta : ℝ} (hb : 0 < b) (hc : 0 < c) (hsigma : sigma = √(b * c)) (htheta : theta = b * c⁻¹) : sigma ^ (-(1 / 2)) * (sigma ^ (1 / 2) - b * sigma ^ (-(1 / 2))) = 1 - √theta

Coefficient identity for the scaled centered special vector q_e.

theorem HCPolySupport.Book.Ch05.Section54.GoodScale.sigmaHat_mul_specialP_centering_coeff_sq_eq {b c sigma theta : ℝ} (hb : 0 < b) (hc : 0 < c) (hsigma : sigma = √(b * c)) (htheta : theta = b * c⁻¹) : sigma * (c⁻¹ * sigma ^ (1 / 2) - sigma ^ (-(1 / 2))) ^ 2 = (√theta - 1) ^ 2

Squared scalar coefficient identity for the centered special vector p_e.

theorem HCPolySupport.Book.Ch05.Section54.GoodScale.inv_sigmaHat_mul_specialQ_centering_coeff_sq_eq {b c sigma theta : ℝ} (hb : 0 < b) (hc : 0 < c) (hsigma : sigma = √(b * c)) (htheta : theta = b * c⁻¹) : sigma⁻¹ * (sigma ^ (1 / 2) - b * sigma ^ (-(1 / 2))) ^ 2 = (√theta - 1) ^ 2

Squared scalar coefficient identity for the centered special vector q_e.