High-contrast homogenization: Provider.Quenched.Prop211Rebase

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

The one-time coarse-ellipticity rebase

This is the unit-range specialization of the renormalization of the coarse-ellipticity assumptions. All numerical parameters are selected before the probability law. The law-dependent choice is only the triadic bracket of the original polynomial base and the entry generation supplied by the entry theorem.

theorem HCPolySupport.HighContrast.Quenched.exists_prop211_rebase_provider (d : ℕ) (hd : 2 ≤ d) {cSc g cStar Centry : ℝ} : cStar ∈ Set.Ioo 0 cSc → g ∈ Set.Ico 0 1 → 0 < Centry → ∃ (Crebase : ℝ), 0 < Crebase ∧ Centry ≤ Crebase ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Psi : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P g E Psi K S → (∃ (mEnt : ℕ), ↑mEnt ≤ ⌈Centry * Real.logb 3 (2 + aspectRatio E * K)⌉ ∧ annealedContrast P ↑mEnt - 1 ≤ cStar ∧ 3 ^ mEnt ≤ 3 * (2 + aspectRatio E * K) ^ Centry) → ∃ (nBase : ℕ) (Pbase : MeasureTheory.Measure (CoeffSpace d)) (gBase : ℝ) (Ebase : BlockMat d) (PsiBase : ℝ → ℝ) (Kbase : ℝ) (Sbase : CoeffSpace d → ℝ), gBase = (1 + g) / 2 ∧ MeasureTheory.IsProbabilityMeasure Pbase ∧ IsStationaryLaw Pbase ∧ IsUnitRangeLaw Pbase ∧ CoarseEllipticityDagger Pbase gBase Ebase PsiBase Kbase Sbase ∧ annealedContrast Pbase 0 - 1 ≤ cStar ∧ blockContrast Ebase ≤ 1 + cSc ∧ (∀ (j : ℕ), annealedContrast Pbase ↑j = annealedContrast P ↑(nBase + j)) ∧ (∀ (j : ℕ), annealedBlock Pbase (centeredCube d ↑j) = annealedBlock P (centeredCube d ↑(nBase + j))) ∧ 3 ^ nBase ≤ (2 + aspectRatio E * K) ^ Crebase ∧ 2 + aspectRatio Ebase * Kbase ≤ (2 + aspectRatio E * K) ^ Crebase

The one-time rebase provider used by the annealed-to-quenched step.