Coarse-graining support: Support.Deterministic.MultiscaleQuantitiesBasic.Foundation.Geometric

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

theorem HCPolySupport.geometricWeight_one_shift {s : ℝ} (h n : ℕ) : geometricWeight s 1 n = Real.rpow 3 (s * ↑h) * geometricWeight s 1 (n + h)

theorem HCPolySupport.rpow_neg_mul_nat_succ_eq (s : ℝ) (n : ℕ) : Real.rpow 3 (-s * ↑(n + 1)) = Real.rpow 3 (-s) * Real.rpow 3 (-s * ↑n)

theorem HCPolySupport.summable_rpow_neg_s_nat_mul_of_summable_geometricWeight_one {H : ℕ → ℝ} {s : ℝ} (hs : 0 < s) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * H n) : Summable fun (n : ℕ) => Real.rpow 3 (-s * ↑n) * H n

theorem HCPolySupport.summable_rpow_neg_s_nat_succ_mul_sub_of_summable_geometricWeight_one {H : ℕ → ℝ} {s : ℝ} (hs : 0 < s) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * H n) : Summable fun (n : ℕ) => Real.rpow 3 (-s * ↑(n + 1)) * (H (n + 1) - H n)

theorem HCPolySupport.tsum_geometricWeight_one_eq_zero_add_tsum_rpow_neg_s_nat_succ_mul_sub {H : ℕ → ℝ} {s : ℝ} (hs : 0 < s) (hsum : Summable fun (n : ℕ) => geometricWeight s 1 n * H n) : ∑' (n : ℕ), geometricWeight s 1 n * H n = H 0 + ∑' (n : ℕ), Real.rpow 3 (-s * ↑(n + 1)) * (H (n + 1) - H n)

theorem HCPolySupport.tsum_geometricWeight_one_le_of_monotone {H : ℕ → ℝ} (hmono : Monotone H) (hnonneg : ∀ (n : ℕ), 0 ≤ H n) {t s : ℝ} (ht : 0 < t) (hts : t < s) (hsum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * H n) : ∑' (n : ℕ), geometricWeight s 1 n * H n ≤ ∑' (n : ℕ), geometricWeight t 1 n * H n

theorem HCPolySupport.geometricDiscount_eq_mul_one (s q : ℝ) : geometricDiscount s q = geometricDiscount (s * q) 1

theorem HCPolySupport.geometricWeight_eq_mul_one (s q : ℝ) (n : ℕ) : geometricWeight s q n = geometricWeight (s * q) 1 n

theorem HCPolySupport.summable_geometricWeight {s q : ℝ} (hsq : 0 < s * q) : Summable fun (n : ℕ) => geometricWeight s q n

theorem HCPolySupport.tsum_geometricWeight_eq_one {s q : ℝ} (hsq : 0 < s * q) : ∑' (n : ℕ), geometricWeight s q n = 1

theorem HCPolySupport.geometricWeight_shift {s q : ℝ} (h n : ℕ) : geometricWeight s q n = Real.rpow 3 (s * q * ↑h) * geometricWeight s q (n + h)

theorem HCPolySupport.summable_geometricWeight_mul_of_nonneg_of_le {H : ℕ → ℝ} {s q C : ℝ} (hsq : 0 < s * q) (hnonneg : ∀ (n : ℕ), 0 ≤ H n) (hbound : ∀ (n : ℕ), H n ≤ C) : Summable fun (n : ℕ) => geometricWeight s q n * H n

theorem HCPolySupport.summable_geometricWeight_of_lt {H : ℕ → ℝ} (hnonneg : ∀ (n : ℕ), 0 ≤ H n) {q t s : ℝ} (hq : 0 < q) (ht : 0 < t) (hts : t < s) (hsum_t : Summable fun (n : ℕ) => geometricWeight t q n * H n) : Summable fun (n : ℕ) => geometricWeight s q n * H n

theorem HCPolySupport.tsum_geometricWeight_le_of_monotone {H : ℕ → ℝ} (hmono : Monotone H) (hnonneg : ∀ (n : ℕ), 0 ≤ H n) {q t s : ℝ} (hq : 0 < q) (ht : 0 < t) (hts : t < s) (hsum_t : Summable fun (n : ℕ) => geometricWeight t q n * H n) : ∑' (n : ℕ), geometricWeight s q n * H n ≤ ∑' (n : ℕ), geometricWeight t q n * H n

theorem HCPolySupport.self_le_tsum_geometricWeight_of_monotone {H : ℕ → ℝ} (hmono : Monotone H) {s q : ℝ} (hsq : 0 < s * q) (hsum : Summable fun (n : ℕ) => geometricWeight s q n * H n) : H 0 ≤ ∑' (n : ℕ), geometricWeight s q n * H n

theorem HCPolySupport.summable_rpow_of_nonneg_of_one_le {f : ℕ → ℝ} {p : ℝ} (hp : 1 ≤ p) (hf_nonneg : ∀ (n : ℕ), 0 ≤ f n) (hf_sum : Summable f) : Summable fun (n : ℕ) => (f n).rpow p

theorem HCPolySupport.tsum_rpow_le_rpow_tsum_of_nonneg {f : ℕ → ℝ} {p : ℝ} (hp : 1 ≤ p) (hf_nonneg : ∀ (n : ℕ), 0 ≤ f n) (hf_sum : Summable f) : ∑' (n : ℕ), (f n).rpow p ≤ (∑' (n : ℕ), f n).rpow p

@[simp]

theorem HCPolySupport.multiscale_ellipticity_LambdaSq_finite_eq {d : ℕ} (Q : TriadicCube d) (s q : ℝ) (a : CoeffField d) : LambdaSq Q s (MultiscaleExponent.finite q) a = LambdaSqFinite Q s q a

@[simp]

theorem HCPolySupport.multiscale_ellipticity_LambdaSq_infinity_eq {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : CoeffField d) : LambdaSq Q s MultiscaleExponent.infinity a = LambdaSqInfinity Q s a

@[simp]

theorem HCPolySupport.multiscale_ellipticity_lambdaSq_finite_eq {d : ℕ} (Q : TriadicCube d) (s q : ℝ) (a : CoeffField d) : lambdaSq Q s (MultiscaleExponent.finite q) a = lambdaSqFinite Q s q a

@[simp]

theorem HCPolySupport.multiscale_ellipticity_lambdaSq_infinity_eq {d : ℕ} (Q : TriadicCube d) (s : ℝ) (a : CoeffField d) : lambdaSq Q s MultiscaleExponent.infinity a = lambdaSqInfinity Q s a

@[simp]

theorem HCPolySupport.scaleResponseAtScale_finite_eq {d : ℕ} (Q : TriadicCube d) (k : ℤ) (p : ℝ) (a : CoeffField d) (a0 : Mat d) : scaleResponseAtScale Q k (MultiscaleExponent.finite p) a a0 = (finsetAverage (descendantsAtScale Q k) fun (R : TriadicCube d) => (normalizedBlockResponseMax R a a0).rpow (p / 2)).rpow (1 / p)

@[simp]

theorem HCPolySupport.scaleResponseAtScale_infinity_eq {d : ℕ} (Q : TriadicCube d) (k : ℤ) (a : CoeffField d) (a0 : Mat d) : scaleResponseAtScale Q k MultiscaleExponent.infinity a a0 = (maxDescendantNormalizedBlockResponseAtScale Q k a a0).rpow (1 / 2)