High-contrast homogenization: Entry.Multiscale.Global.ScalarLemmas

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

Scalar lemmas of the selection run

The real-arithmetic layer of the global selection argument p.global.selection: the scaled-logarithm growth, contraction and span bounds (e.global.selection.scalar.span), the comparison tolerance ε and comparison choice (e.global.selection.comparison.choice), the weight choice, the eccentricity arithmetic (e.global.selection.eccentricity), and the scale and containment arithmetic (e.global.selection.lower.scale) that fixes the outer constants in the required order.

§A Scalar lemmas (p.global.selection)

theorem HCPolySupport.HighContrast.Multiscale.scalar_growth_bound (η Q C x y : ℝ) (hη : η ∈ Set.Ioc 0 1) (hC : 1 ≤ C) (hQ : 0 ≤ Q) (hx : 0 ≤ x) (hy : 0 ≤ y) : η * Real.log (1 + η⁻¹ * (Real.exp (Q * y) * x / 8 + C * (Real.exp (Q * y) - 1))) ≤ η * Real.log (1 + x / (8 * η)) + Q * (1 + C) * y

p.global.selection, integrated: the scaled logarithm grows at most linearly in y. Proof idea: with u = x/(8η), w = exp (Q y), Bernoulli gives 1 + u w + (C/η)(w-1) ≤ (1+u) w^(1+C/η).

theorem HCPolySupport.HighContrast.Multiscale.scalar_contraction (η x : ℝ) (hη : 0 < η) (hx : η < x) : η * Real.log (1 + x / (8 * η)) ≤ η * Real.log (1 + x / η) - η * Real.log (16 / 9)

p.global.selection: for x > η, η log(1 + x/(8η)) ≤ η log(1 + x/η) - η log(16/9).

theorem HCPolySupport.HighContrast.Multiscale.scalar_span (η Q C ℓ x x' y : ℝ) (hη : η ∈ Set.Ioc 0 1) (hC : 0 ≤ C) (hℓ : 1 ≤ ℓ) (hQ : 0 ≤ Q) (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hy : 0 ≤ y) (hx'0 : 0 ≤ x') (hx' : x' ≤ C * ℓ * (x + (Real.exp (Q * y) - 1))) : η * Real.log (1 + x' / η) ≤ Real.log (1 + C * ℓ) + Q * y

e.global.selection.scalar.span. Proof idea: x' ≤ C ℓ exp (Q y), then (1 + Cℓ/η)^η ≤ 1 + Cℓ by Bernoulli with exponent η ≤ 1.

theorem HCPolySupport.HighContrast.Multiscale.comparison_choice (C : ℝ) (hC : 1 ≤ C) (h : ℕ) (ε₀ : ℝ) (hε₀ : ε₀ ∈ Set.Ioo 0 1) : ∃ ε ∈ Set.Ioc 0 ε₀, ∀ σ ∈ Set.Ioc 0 ε, 1 / 2 * Real.log ((1 + √ε * σ) / (1 - √ε * σ)) + 2 * C * (↑h + 2) * Real.log (1 + √ε * σ) ≤ min (ε / 2) (C * σ / 4)

e.global.selection.comparison.choice: ε ∈ (0, ε₀] depending only on C, h such that, with δ = √ε σ, the comparison terms are below min {ε/2, Cσ/4} for every σ ∈ (0, ε]. Proof idea: δ ≤ ε^(3/2) ≤ 1/2, ½ log((1+δ)/(1-δ)) ≤ 2δ, log(1+δ) ≤ δ.

theorem HCPolySupport.HighContrast.Multiscale.weight_choice (d : ℕ) (hd : 0 < d) (C Q ε σ c L H h : ℝ) (hC : 0 < C) (hε : 0 < ε) (hσ : 0 < σ) : ∃ (a : ℝ), 1 ≤ a ∧ 4 * Q * max 1 C ≤ a * C / ↑d ∧ Real.log (1 + C * h) + c ≤ a * ε / 2 ∧ 4 * (Real.log (1 + 2 * C * L) + Real.log (1 + C * H) + c) ≤ a * C * ε * σ

e.global.selection.weight.choice: the weight a ≥ 1 exists (Archimedean).

theorem HCPolySupport.HighContrast.Multiscale.exp_sub_one_le_rpow (Q d σ γ : ℝ) (hQ : 0 ≤ Q) (hd : 0 ≤ d) (hσ : σ ∈ Set.Ioc 0 1) (hγ : γ ∈ Set.Ico 0 1) : Real.exp (Q * d * σ) - 1 ≤ Q * d * Real.exp (Q * d) * σ ^ ((1 - γ) / 8)

p.global.selection: exp(Q d σ) - 1 ≤ Q d exp(Q d) σ^((1-γ)/8) for σ ∈ (0,1], the constant free of σ. Proof idea: exp t - 1 ≤ t exp t for t ≥ 0, and σ ≤ σ^((1-γ)/8) since σ ≤ 1.

theorem HCPolySupport.HighContrast.Multiscale.source_threshold_mono (x y C C' : ℝ) (j : ℤ) (hx : 0 ≤ x) (hy : 0 ≤ y) (hCC : C' ≤ C) (hj : ⌈y + C * x⌉ ≤ j) : ⌈C' * x⌉ ≤ j

The bundled lower bound e.global.selection.lower.scale implies every weaker source threshold.

theorem HCPolySupport.HighContrast.Multiscale.eccentricity_arith (ε C₁ : ℝ) (hε : 0 < ε) (hC₁ : 0 ≤ C₁) : ∃ (C : ℝ), 0 < C ∧ ∀ (AR : ℝ), 0 ≤ AR → Real.exp (ε * (↑⌈C₁ * Real.logb 3 (2 + AR)⌉ + 1)) ≤ (2 + AR) ^ C

p.global.selection arithmetic of e.global.selection.eccentricity: after at most ⌈C₁ log₃(2+Π)⌉ + 1 projective steps of size ε, exp (ε (J+1)) ≤ (2+Π)^C with C = C(ε, C₁) free of Π.

theorem HCPolySupport.HighContrast.Multiscale.scales_arith (Cinit C₁ L H h : ℝ) (hCi : 0 ≤ Cinit) (hC₁ : 0 ≤ C₁) (hL : 0 ≤ L) (hH : 0 ≤ H) (hh : 0 ≤ h) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : ℝ), 1 / 2 ≤ x → ∀ (B : ℝ), ↑⌈B * x⌉ + ↑⌈Cinit * x⌉ + (2 * L + H + h) * (↑⌈C₁ * x⌉ + 2) + L + H ≤ ↑⌈(B + C) * x⌉

p.global.selection-p.global.selection arithmetic of e.global.selection.scales: the entry generation plus J + 2 steps of length ≤ 2L + H + h plus the final L + H fit under ⌈(B + C) log₃(2+Π)⌉.

theorem HCPolySupport.HighContrast.Multiscale.containment_arith (Cinit C₁ L H h ε d : ℝ) (hCi : 0 ≤ Cinit) (hC₁ : 0 ≤ C₁) (hL : 0 ≤ L) (hH : 0 ≤ H) (hh : 0 ≤ h) (hε : 0 ≤ ε) (hd : 1 ≤ d) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : ℝ), 1 / 2 ≤ x → ∀ (B : ℝ), 0 ≤ B → ∀ (jStar : ℤ), ⌈C * (B + 1) * x⌉ ≤ jStar → ↑jStar + ↑⌈B * x⌉ + ↑⌈Cinit * x⌉ + (2 * L + H + h) * (↑⌈C₁ * x⌉ + 2) + ↑⌈Real.logb 3 (2 * √d) + ε * (↑⌈C₁ * x⌉ + 1) / Real.log 3⌉ ≤ 2 * ↑jStar

p.global.selection arithmetic of the containment budget: n₀ + (2L+H+h)(J+2) + ⌈log₃(2√d) + ε(J+1)/log 3⌉ ≤ 2 jStar follows from the entry bound and the lower scale e.global.selection.lower.scale once C is large.