High-contrast homogenization: Provider.Regularity.FiniteAffineGradientExcessRateSelection

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

theorem HCPolySupport.HighContrast.exists_nat_integer_rate_deterministic_le (depth p : ℕ) (hp : 0 < p) (eta C₀ Cc Ce : ℝ) (heta : eta < 1 - 1 / (2 * ↑p)) (hC₀ : 0 < C₀) (hCc : 0 < Cc) (hCe : 0 < Ce) : ∃ (t : ℕ), Cc * (C₀ * (1 / 3) ^ ((2 * p - 1) * t) * Ce) ≤ 1 / 4 * Real.rpow 3 (-eta * ↑(depth + 2 * p * t + 4))

The integer-rate deterministic coefficient eventually beats the printed real-exponent target whenever eta is below its effective rate.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteAffineGradientExcessRateContractionConstants (d : ℕ) [NeZero d] (s eta : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) (_heta0 : 0 ≤ eta) (heta1 : eta < 1) (C : ℝ) (hC : 1 ≤ C) : ∃ (H : ℕ), 0 < H ∧ ∃ (c : ℝ), 0 < c ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n m : ℤ) (Q : ℤ → Mat d), delta ∈ Set.Ioc 0 c → ScalarIdentityGoodMaxOnInterval a s delta n m → IsFiniteAffineSlopeFamily a delta C n m Q → ∀ k ∈ Finset.Icc n m, k - ↑H ∈ Finset.Icc n m → ∀ (u : Book.Ch03.CubeSolution (originCube d m) a), finiteAffineGradientExcess a (k - ↑H) m u ≤ ENNReal.ofReal (1 / 2 * Real.rpow 3 (-eta * ↑H)) * finiteAffineGradientExcess a k m u

The ruled best-fit Step-1 recurrence with the printed real exponent.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteAffineGradientExcessRateContractionProviderConstants (d : ℕ) [NeZero d] (s eta : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) (heta0 : 0 ≤ eta) (heta1 : eta < 1) : ∃ (C : ℝ) (c : ℝ), 1 ≤ C ∧ 0 < c ∧ ∃ (H : ℕ), 0 < H ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n m : ℤ), n < m → delta ∈ Set.Ioc 0 c → ScalarIdentityGoodMaxOnInterval a s delta n m → ∃ (Q : ℤ → Mat d), IsFiniteAffineSlopeFamily a delta C n m Q ∧ ∀ k ∈ Finset.Icc n m, k - ↑H ∈ Finset.Icc n m → ∀ (u : Book.Ch03.CubeSolution (originCube d m) a), finiteAffineGradientExcess a (k - ↑H) m u ≤ ENNReal.ofReal (1 / 2 * Real.rpow 3 (-eta * ↑H)) * finiteAffineGradientExcess a k m u

Caller-facing ruled-family Step 1 with the printed real exponent.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteAffineGradientExcessRateDiscreteDecayConstants (d : ℕ) [NeZero d] (s eta : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) (heta0 : 0 ≤ eta) (heta1 : eta < 1) : ∃ (C : ℝ) (c : ℝ), 1 ≤ C ∧ 0 < c ∧ ∃ (H : ℕ), 0 < H ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n m : ℤ), n < m → delta ∈ Set.Ioc 0 c → ScalarIdentityGoodMaxOnInterval a s delta n m → ∃ (Q : ℤ → Mat d), IsFiniteAffineSlopeFamily a delta C n m Q ∧ ∀ (u : Book.Ch03.CubeSolution (originCube d m) a), have gap := (m - n).toNat; have t := gap / H; have R := gap % H; finiteAffineGradientExcess a n m u ≤ ENNReal.ofReal ↑((3 ^ d) ^ R) * (ENNReal.ofReal (1 / 2 * Real.rpow 3 (-eta * ↑H)) ^ t * finiteAffineGradientExcess a m m u)

Arbitrary-gap Step-1 decay with the terminal remainder band explicit.

theorem HCPolySupport.HighContrast.exists_scalarIdentityFiniteAffineGradientExcessRealRateDecayConstants (d : ℕ) [NeZero d] (s eta : ℝ) (hs : 0 < s) (hs_lt : s < 1 / 2) (heta0 : 0 ≤ eta) (heta1 : eta < 1) : ∃ (Cfamily : ℝ) (c : ℝ) (Cdec : ℝ), 1 ≤ Cfamily ∧ 0 < c ∧ 0 < Cdec ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (delta : ℝ) (n m : ℤ), n < m → delta ∈ Set.Ioc 0 c → ScalarIdentityGoodMaxOnInterval a s delta n m → ∃ (Q : ℤ → Mat d), IsFiniteAffineSlopeFamily a delta Cfamily n m Q ∧ ∀ (u : Book.Ch03.CubeSolution (originCube d m) a), finiteAffineGradientExcess a n m u ≤ ENNReal.ofReal (Cdec * Real.rpow 3 (-eta * ↑(m - n))) * finiteAffineGradientExcess a m m u

Full Step-1 decay in the printed real-exponent form, with the ruled best-fit slope family produced in the same existential package.