High-contrast homogenization: Entry.Multiscale.ScaleSelection.ParameterArithmetic

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

Real arithmetic of the parameter choice

Group A of the printed proof (p.scale.selection): the elementary exponential and logarithm inequalities behind the service reduction, the membership and comparison facts for the bridge tolerance √ε σ and the transport ratio σ^{(1-γ)/8}, the two length conditions satisfied by selectionLength, the old-grid smallness that fixes ε₁, the scale separation, the choice of ε₀, and the exhaustiveness of the five guarded alternatives.

Part of the proof of p.scale.selection. Conventions of the group: q = 𝒬(𝔪) is Geometry.explicitRoundedGrid jStar m; the printed data are h = 2Q, c = c₀, L(ε,σ) = selectionLength L₀ σ and B₀(ε,σ) = max 1 (max (B₀^bridge (√ε σ) L) (2 C_tr (L+1))); √ε is the printed ε^{1/2}; the source lower scale e.source.lower.scale is carried wherever j_* appears with the law, and no integrability, finiteness or measurability premise is added anywhere. Unused hypothesis binders of a statement are underscore-prefixed.

The declaration text of this file is the closed skeleton's, copied unchanged; only this header, the imports and the namespace frame are new.

Group A — real arithmetic of the parameter choice (p.scale.selection)

theorem HCPolySupport.HighContrast.Multiscale.exp_sub_one_le_two_mul (x : ℝ) (h0 : 0 ≤ x) (hx : x ≤ Real.log 2) : Real.exp x - 1 ≤ 2 * x

theorem HCPolySupport.HighContrast.Multiscale.service_reduction (a b x C : ℝ) (hb : 0 ≤ b) (hC : 0 ≤ C) (h0 : 0 ≤ x) (hx : x ≤ Real.log 2) (h : a ≤ 1 / 8 * Real.exp x * b + C * (Real.exp x - 1)) : a ≤ 1 / 4 * b + 2 * C * x

p.scale.selection: the service reduction ⅛e^x b + C(e^x−1) ≤ ¼b + 2Cx for 0 ≤ x ≤ log 2.

theorem HCPolySupport.HighContrast.Multiscale.ceil_mul_le_ceil_mul (B₀ B x : ℝ) (hB : B₀ ≤ B) (hx : 0 ≤ x) : ⌈B₀ * x⌉ ≤ ⌈B * x⌉

theorem HCPolySupport.HighContrast.Multiscale.logb_two_add_aspectRatio_nonneg {d : ℕ} (E : BlockMat d) : 0 ≤ Real.logb 3 (2 + aspectRatio E)

theorem HCPolySupport.HighContrast.Multiscale.half_le_logb_two_add (Pi : ℝ) (hPi : 0 ≤ Pi) : 1 / 2 ≤ Real.logb 3 (2 + Pi)

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

theorem HCPolySupport.HighContrast.Multiscale.bridge_tolerance_mem (ε σ : ℝ) (hε : ε ∈ Set.Ioc 0 1) (hσ : σ ∈ Set.Ioc 0 ε) : √ε * σ ∈ Set.Ioc 0 1

theorem HCPolySupport.HighContrast.Multiscale.bridge_tolerance_le_quarter (ε σ : ℝ) (hε : ε ∈ Set.Ioc 0 (1 / 4)) (hσ : σ ∈ Set.Ioc 0 ε) : √ε * σ ∈ Set.Icc 0 (1 / 4)

theorem HCPolySupport.HighContrast.Multiscale.transport_rho_mem (σ γ : ℝ) (hσ : σ ∈ Set.Ioc 0 1) (hγ : γ ∈ Set.Ico 0 1) : σ ^ ((1 - γ) / 8) ∈ Set.Ioc 0 1

theorem HCPolySupport.HighContrast.Multiscale.bridge_tolerance_le_rho (ε σ γ : ℝ) (hε : ε ∈ Set.Ioc 0 1) (hσ : σ ∈ Set.Ioc 0 ε) (hγ : γ ∈ Set.Ico 0 1) : √ε * σ ≤ σ ^ ((1 - γ) / 8)

p.scale.selection defines δ = ε^{1/2}σ and ρ = σ^{(1−γ)/8}; p.scale.selection gives the comparison δ ≤ ρ, for which δ ≤ σ ≤ ρ is the elementary justification.

theorem HCPolySupport.HighContrast.Multiscale.one_le_selectionLength (L₀ : ℕ) (hL₀ : 1 ≤ L₀) (σ : ℝ) : 1 ≤ selectionLength L₀ σ

theorem HCPolySupport.HighContrast.Multiscale.selectionLength_bridge_condition (L₀ : ℕ) (ε σ : ℝ) (hε : ε ∈ Set.Ioc 0 1) (hσ : σ ∈ Set.Ioc 0 ε) : ↑L₀ + ⌈Real.logb 3 (√ε * σ)⁻¹⌉ ≤ ↑(selectionLength L₀ σ)

p.scale.selection: the chosen length satisfies the short-bridge length condition at the smaller tolerance ε^{1/2}σ.

theorem HCPolySupport.HighContrast.Multiscale.selectionLength_transport_condition (C : ℝ) (L₀ : ℕ) (hC : C ≤ ↑L₀) (σ γ : ℝ) (hσ : σ ∈ Set.Ioc 0 1) (hγ : γ ∈ Set.Ico 0 1) : C + Real.logb 3 (σ ^ ((1 - γ) / 8))⁻¹ ≤ ↑(selectionLength L₀ σ)

p.scale.selection: with L₀ ≥ C, the chosen length satisfies L ≥ C + log₃(ρ⁻¹) at ρ = σ^{(1−γ)/8}.

theorem HCPolySupport.HighContrast.Multiscale.selectionLength_le (L₀ : ℕ) (σ : ℝ) (hσ : σ ∈ Set.Ioc 0 1) : ↑(selectionLength L₀ σ) ≤ ↑L₀ + 1 + 3 / 2 * Real.logb 3 σ⁻¹

theorem HCPolySupport.HighContrast.Multiscale.rpow_mul_logb_le (α σ : ℝ) (hα : 0 < α) (hσ : σ ∈ Set.Ioc 0 1) : σ ^ α * Real.logb 3 σ⁻¹ ≤ 1 / (α * Real.log 3)

p.scale.selection: σ^α log₃(σ⁻¹) is bounded on (0,1] for α > 0.

theorem HCPolySupport.HighContrast.Multiscale.three_rpow_selectionLength_le (L₀ : ℕ) (σ γ : ℝ) (hσ : σ ∈ Set.Ioc 0 1) (hγ : γ ∈ Set.Ico 0 1) : 3 ^ (1 / 2 * (1 - γ) * ↑(selectionLength L₀ σ)) ≤ 3 ^ (1 / 2 * (1 - γ) * (↑L₀ + 1)) * σ ^ (-(3 / 4) * (1 - γ))

p.scale.selection: 3^{½(1−γ)L} ≤ 3^{½(1−γ)(L₀+1)} σ^{−¾(1−γ)} for the chosen L.

theorem HCPolySupport.HighContrast.Multiscale.old_grid_smallness_arith (C' : ℝ) (hC' : 0 < C') (L₀ : ℕ) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (ε₁ : ℝ), 0 < ε₁ ∧ ε₁ ≤ 1 ∧ ∀ (ε σ : ℝ), ε ∈ Set.Ioc 0 ε₁ → σ ∈ Set.Ioc 0 ε → C' * (1 + ↑(selectionLength L₀ σ)) * ε * σ ≤ 3 ^ (-(1 / 2) * (1 - γ) * ↑(selectionLength L₀ σ)) * σ ^ ((1 - γ) / 8)

p.scale.selection: the old-grid smallness is a smallness of ε₀ alone.

theorem HCPolySupport.HighContrast.Multiscale.scale_separation_arith (C ε L X Pi k n j B : ℝ) (hC : 0 < C) (hε : 0 < ε) (hL : 1 ≤ L) (hX : 1 ≤ X) (hPi : 0 ≤ Pi) (hkn : k ≤ n) (hB : 2 * C * (L + 1) ≤ B) (hLε : 2 * C * ε ≤ L * Real.log 3) (hecc : 1 / 2 * Real.log X ≤ ε / L * (k - j - ↑⌈B * Real.logb 3 (2 + Pi)⌉)) : C * (L + Real.logb 3 ((2 + Pi) * X)) ≤ n - j

p.scale.selection: the transport scale separation from the eccentricity input, B ≥ 2C(L+1) and L log 3 ≥ 2Cε.

theorem HCPolySupport.HighContrast.Multiscale.exists_eps0 (d : ℕ) (_hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (C Ctr c₀ ε₁ : ℝ) (L₀ : ℕ) (hC : 0 < C) (hCtr : 0 < Ctr) (hc₀ : c₀ ∈ Set.Ioo 0 1) (hε₁ : 0 < ε₁) (hL₀ : 1 ≤ L₀) : ∃ ε₀ ∈ Set.Ioo 0 1, ε₀ ≤ 1 / 4 ∧ ε₀ ≤ (c₀ / (↑d + 1)) ^ 2 ∧ ↑(bigQ d γ) * ↑d * ε₀ ≤ Real.log 2 ∧ C * ε₀ ^ ((1 - γ) / 8) ≤ 1 ∧ ε₀ ≤ ε₁ ∧ 2 * Ctr * ε₀ ≤ ↑L₀ * Real.log 3

p.scale.selection: the outer ε₀(d,γ), chosen after C, C_tr, c₀, L₀ and the smallness threshold ε₁.

theorem HCPolySupport.HighContrast.Multiscale.bridge_smallness_arith (d : ℕ) (_hd : 2 ≤ d) (c c₀ ε σ a D Δ : ℝ) (hc : c ∈ Set.Ioo 0 1) (hc₀ : c₀ ∈ Set.Ioo 0 1) (hε : 0 < ε) (hεc : ε ≤ (c₀ / (↑d + 1)) ^ 2) (hσ : 0 < σ) (hD : a + D ≤ c * ε * σ) (hΔ : (↑d)⁻¹ * Δ ≤ ε * σ) : a + D + Δ ≤ c₀ * (√ε * σ)

p.scale.selection: 𝒫+D+Δ ≤ (c+d)εσ ≤ c₀ ε^{1/2} σ once ε ≤ (c₀/(d+1))².

theorem HCPolySupport.HighContrast.Multiscale.bridge_eccentricity_arith (y ε c₀ L k j a B₀ B : ℝ) (hy : 0 ≤ y) (hε : 0 < ε) (h2ε : 2 * ε ≤ c₀) (hL : 0 < L) (ha : 0 ≤ a) (hB : B₀ ≤ B) (hecc : 1 / 2 * y ≤ ε / L * (k - j - ↑⌈B * a⌉)) : y ≤ c₀ / L * (k - j - ↑⌈B₀ * a⌉)

p.scale.selection: the bridge eccentricity from the input eccentricity, 2ε ≤ c₀, B ≥ B₀.

theorem HCPolySupport.HighContrast.Multiscale.geometry_eccentricity_output_arith (y y' ε L k n j b : ℝ) (hy' : y' ≤ y + ε) (hε : 0 < ε) (hL : 1 ≤ L) (hkn : k ≤ n) (hecc : y ≤ ε / L * (k - j - b)) : y' ≤ ε / L * (n + L - j - b)

p.scale.selection: the output eccentricity after a change of geometry.

theorem HCPolySupport.HighContrast.Multiscale.alternatives_exhaustive (k n : ℤ) (hkn : k ≤ n) (a η x σ y t : ℝ) : k = n ∨ k < n ∧ a > η ∧ x ≤ σ ∨ k < n ∧ a ≤ η ∧ y ≤ t ∨ k < n ∧ a > η ∧ x > σ ∨ k < n ∧ a ≤ η ∧ y > t

p.scale.selection: the five guarded alternatives are exhaustive under k ≤ n.

theorem HCPolySupport.HighContrast.Multiscale.bridge_smallness_arith_combined (d : ℕ) (hd : 2 ≤ d) (c c₀ ε σ A : ℝ) (hc : c ∈ Set.Ioo 0 1) (hc₀ : c₀ ∈ Set.Ioo 0 1) (hε : 0 < ε) (hεc : ε ≤ (c₀ / (↑d + 1)) ^ 2) (hσ : 0 < σ) (hA : A ≤ (c + ↑d) * ε * σ) : A ≤ c₀ * (√ε * σ)

p.scale.selection, in the combined form stated by Selects: 𝒫+D+Δ ≤ (c+d)εσ ≤ c₀ ε^{1/2} σ once ε ≤ (c₀/(d+1))².