High-contrast homogenization: Provider.Quenched.SmallContrastCarryBack

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

Carrying the hcore body back from the recentered law stage 2b, bottom. put the four isotropy

certificates at the recentered block E', at the cost of running the account at recenteredLaw P hg rather than at P. This file pays that cost back.

The hcore conclusion speaks only of annealedContrast, and's annealedContrast_recenteredLaw says that quantity is invariant under recentering. So the carry-back is a rewrite under the ∀ j, with no loss: the delay bound 3 ^ m₀ ≤ base ^ Cdelay does not mention the law at all, and the decay bound transports pointwise.

With the top and this bottom half, the recentered route is complete: what remains is the instantiation in between.

theorem HCPolySupport.HighContrast.Quenched.hcore_body_carry_back {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : Mat d} (hg : IsSkewMat g) (hint : ∀ (m : ℤ), HasFiniteAdaptedMean P 1 m) (hpd : ∀ (m : ℤ), Book.Ch02.BlockPosDef (annealedBlock P (centeredCube d m))) {base Cdelay alpha : ℝ} (h : ∃ (m₀ : ℕ), 3 ^ m₀ ≤ base.rpow Cdelay ∧ ∀ (j : ℕ), annealedContrast (recenteredLaw P hg) ↑(m₀ + j) - 1 ≤ Real.rpow 3 (-alpha * ↑j)) : ∃ (m₀ : ℕ), 3 ^ m₀ ≤ base.rpow Cdelay ∧ ∀ (j : ℕ), annealedContrast P ↑(m₀ + j) - 1 ≤ Real.rpow 3 (-alpha * ↑j)

The carry-back. The hcore inner body at the recentered law is the hcore inner body at the original law.