High-contrast homogenization: Entry.Multiscale.PolynomialEntry.Arithmetic

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Arithmetic of the polynomial entry scales

This module proves the elementary numeric estimates that dominate the linear window scales of the polynomial entry by the exponential scale 3 ^ d and convert them into the logarithmic coefficient of t.polynomial.entry.

It establishes the growth bound 2 * d ≤ 3 ^ d together with its monotone form, the positivity and monotonicity of the base-three logarithms log₃ 2, log₃ (2 + x) and log₃ (2 * K), and the resulting real and integer bounds on the entry scale j_*, on the entry constant C assembled from the fixed constants and (3 + d) / log₃ 2, and on the terminal scale. These are the estimates that fix the threshold and the logarithmic coefficient c = log₃ (2 + Π K) appearing in t.polynomial.entry.

theorem HCPolySupport.HighContrast.Multiscale.two_mul_le_three_pow (d : ℕ) : 2 * d ≤ 3 ^ d

For every natural number d, twice d is at most 3 to the power d. This is the elementary growth bound used to dominate the linear scales occurring in t.polynomial.entry by the exponential scale 3 ^ d.

theorem HCPolySupport.HighContrast.Multiscale.two_mul_le_three_pow_of_le (d j : ℕ) (h : d ≤ j) : 2 * d ≤ 3 ^ j

Monotonicity form of two_mul_le_three_pow: if d ≤ j, then 2 * d ≤ 3 ^ j.

theorem HCPolySupport.HighContrast.Multiscale.zero_lt_logb_three_two : 0 < Real.logb 3 2

The base-three logarithm of 2 is positive, so log₃ 2 is a legitimate positive normalising factor for the entry scales of t.polynomial.entry.

theorem HCPolySupport.HighContrast.Multiscale.logb_two_add_nonneg (x : ℝ) (hx : 0 ≤ x) : 0 ≤ Real.logb 3 (2 + x)

For x ≥ 0 the base-three logarithm of 2 + x is nonnegative.

theorem HCPolySupport.HighContrast.Multiscale.logb_two_mul_nonneg_of_one_le (K : ℝ) (hK : 1 ≤ K) : 0 ≤ Real.logb 3 (2 * K)

For K ≥ 1 the base-three logarithm of 2 * K is nonnegative.

theorem HCPolySupport.HighContrast.Multiscale.logb_two_le_logb_two_add (x : ℝ) (hx : 0 ≤ x) : Real.logb 3 2 ≤ Real.logb 3 (2 + x)

Adding a nonnegative quantity inside the argument of the base-three logarithm does not decrease its value below log₃ 2.

theorem HCPolySupport.HighContrast.Multiscale.logb_two_add_le_logb_two_add_mul (x K : ℝ) (hx : 0 ≤ x) (hK : 1 ≤ K) : Real.logb 3 (2 + x) ≤ Real.logb 3 (2 + x * K)

For x ≥ 0 and K ≥ 1, replacing x by x * K in 2 + x only increases the base-three logarithm; this is the monotonicity used when the source term is multiplied by the ellipticity constant K.

theorem HCPolySupport.HighContrast.Multiscale.logb_two_mul_le_two_mul_logb (x K : ℝ) (hx : 1 ≤ x) (hK : 1 ≤ K) : Real.logb 3 (2 * K) ≤ 2 * Real.logb 3 (2 + x * K)

For x ≥ 1 and K ≥ 1, the logarithm of 2 * K is dominated by twice the logarithm of 2 + x * K; this turns the entry constant into a coefficient of the logarithmic scale c = log₃ (2 + Π K) in t.polynomial.entry.

theorem HCPolySupport.HighContrast.Multiscale.le_div_logb_mul (M c : ℝ) (hM : 0 ≤ M) (hc : Real.logb 3 2 ≤ c) : M ≤ M / Real.logb 3 2 * c

For M ≥ 0 and c ≥ log₃ 2, the quantity M / log₃ 2 * c dominates M; this is the normalisation step that lets the linear term 3 + d be paid for by the logarithmic coefficient c in t.polynomial.entry.

noncomputable def HCPolySupport.HighContrast.Multiscale.entryScale (A Csrc a b : ℝ) (d : ℕ) : ℕ

The entry scale j_* of t.polynomial.entry: the integer ceiling of A * a + Csrc * b, shifted up by d.

Equations

• HCPolySupport.HighContrast.Multiscale.entryScale A Csrc a b d = ⌈A * a + Csrc * b⌉.toNat + d

theorem HCPolySupport.HighContrast.Multiscale.le_entryScale (A Csrc a b : ℝ) (d : ℕ) : d ≤ entryScale A Csrc a b d

The entry scale is at least its prescribed shift d.

theorem HCPolySupport.HighContrast.Multiscale.ceil_le_entryScale (A Csrc Csrc' a b : ℝ) (d : ℕ) (hb : 0 ≤ b) (hC : Csrc' ≤ Csrc) : ⌈A * a + Csrc' * b⌉ ≤ ↑(entryScale A Csrc a b d)

If Csrc' ≤ Csrc and b ≥ 0, then the integer ceiling computed with Csrc' is still dominated by the entry scale computed with Csrc.

theorem HCPolySupport.HighContrast.Multiscale.entryScale_le (A Csrc a b : ℝ) (d : ℕ) (h : 0 ≤ A * a + Csrc * b) : ↑(entryScale A Csrc a b d) ≤ A * a + Csrc * b + 1 + ↑d

The entry scale, viewed in ℝ, is at most its real defining expression plus one and the shift d, whenever that expression is nonnegative.

noncomputable def HCPolySupport.HighContrast.Multiscale.entryConst (A B Cg Cresp Csrc : ℝ) (d : ℕ) : ℝ

The entry constant C of t.polynomial.entry, assembled from the fixed constants A, B, Cg, Cresp, Csrc and the logarithmic normalisation (3 + d) / log₃ 2.

Equations

• HCPolySupport.HighContrast.Multiscale.entryConst A B Cg Cresp Csrc d = A + B + Cg + Cresp + 2 * Csrc + (3 + ↑d) / Real.logb 3 2

theorem HCPolySupport.HighContrast.Multiscale.entryConst_pos (A B Cg Cresp Csrc : ℝ) (d : ℕ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hCg : 0 < Cg) (hCresp : 0 ≤ Cresp) (hCsrc : 0 ≤ Csrc) : 0 < entryConst A B Cg Cresp Csrc d

The entry constant is positive as soon as Cg > 0 and the remaining constants are nonnegative.

theorem HCPolySupport.HighContrast.Multiscale.terminal_le_real (j t m : ℤ) (B Cg Cresp a : ℝ) (ht : t ≤ j + ⌈(B + Cg) * a⌉) (hm : m - t ≤ ⌈Cresp * a⌉) : ↑m ≤ ↑j + (B + Cg) * a + Cresp * a + 2

The real terminal scale of t.polynomial.entry: if the integer terminal t is bounded by j + ⌈(B + Cg) * a⌉ and m - t by ⌈Cresp * a⌉, then m is at most the corresponding real logarithmic expression with two units of rounding slack.

theorem HCPolySupport.HighContrast.Multiscale.entry_bound_real (A B Cg Cresp Csrc a b c : ℝ) (d : ℕ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hac : a ≤ c) (hbc : b ≤ 2 * c) (hc : Real.logb 3 2 ≤ c) (hA : 0 ≤ A) (hB : 0 ≤ B) (hCg : 0 ≤ Cg) (hCresp : 0 ≤ Cresp) (hCsrc : 0 ≤ Csrc) (m : ℝ) (hm : m ≤ A * a + Csrc * b + 1 + ↑d + (B + Cg) * a + Cresp * a + 2) : m ≤ entryConst A B Cg Cresp Csrc d * c

The real entry bound of t.polynomial.entry: the terminal value m, already bounded by the sum of the entry scale and the response and terminal scales, is dominated by the entry constant times the logarithmic scale c = log₃ (2 + Π K).

theorem HCPolySupport.HighContrast.Multiscale.entry_bound_int (C c : ℝ) (m : ℤ) (h : ↑m ≤ C * c) : m ≤ ⌈C * c⌉

Integer form of the entry bound: an integer m bounded in ℝ by C * c is bounded by the integer ceiling ⌈C * c⌉.

theorem HCPolySupport.HighContrast.Multiscale.scale_le_terminal (j s t m : ℤ) (B a : ℝ) (hB : 0 ≤ B) (ha : 0 ≤ a) (hs : j + ⌈B * a⌉ ≤ s) (hst : s < t) (htm : t < m) : j ≤ m

The terminal scale exceeds every earlier scale: if j + ⌈B * a⌉ ≤ s < t < m, then j ≤ m.