High-contrast homogenization: Provider.Quenched.SmallContrastBootstrapTransferInputs

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

The corrected-tilt transfer inputs

The corrected tilt transfer consumes, at the corrected halfway scale n = ⌊m/2⌋ + n₀ of the midpoint-scale identity, four inputs: the reverse Loewner adapter, the unit cap on the absorbed size, the unit cap on the hatted defect, and the decaying error clause. The first, second and fourth are supplied here from the reverse adapter with its generation-free law factor; the third is the bootstrap smallness at tolerance one.

The only arithmetic in this file is the passage from the adapter's integer scale difference -(m − n) to the natural-number difference the corrected transfer writes, which needs n ≤ m.

theorem HCPolySupport.HighContrast.Quenched.three_rpow_neg_intCast_sub_eq {a b : ℕ} (hab : b ≤ a) : 3 ^ (-(↑↑a - ↑↑b)) = Real.rpow 3 (-↑(a - b))

The adapter's triadic error factor written with the natural-number scale difference of the corrected halfway transfer.

theorem HCPolySupport.HighContrast.Quenched.exists_corrected_tilt_transfer_inputs (d : ℕ) (hd : 2 ≤ d) (g : ℝ) (hg : g ∈ Set.Ico 0 1) : ∃ (CB : ℝ), 0 < CB ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P g E Ψ K S → ∀ (Cd : ℝ), max 1 (12 * ↑d * √↑d) ≤ Cd → ∀ (sK : ℤ), 0 ≤ sK → growthBar K ≤ 3 ^ sK → ∀ (l : ℤ), ↑(kZero d) ≤ l → ∀ (mAl : Mat d), Matrix.PosDef mAl → ∀ (G : ℕ), ‖roundedGrid l mAl‖ * √↑d ≤ 3 ^ G → ∀ (n₀ mOut : ℕ), 0 < Prop42Scalar.correctedTiltScale n₀ mOut → Prop42Scalar.correctedTiltScale n₀ mOut < mOut → l ≤ ↑(Prop42Scalar.correctedTiltScale n₀ mOut) → 0 ≤ ↑(Prop42Scalar.correctedTiltScale n₀ mOut) + ↑G - 1 - sK → ∀ (A : ℝ), CB * reverseAdapterFactor Cd g K E mAl G ≤ A → A * Real.rpow 3 (-↑(mOut - Prop42Scalar.correctedTiltScale n₀ mOut)) ≤ 1 → ∃ (c : ℝ), 0 ≤ c ∧ BlockMatLoewnerLE (blockSub (annealedBlock P (centeredCube d ↑mOut)) (adaptedMean P (roundedGrid l mAl) ↑(Prop42Scalar.correctedTiltScale n₀ mOut))) (blockScale c E) ∧ c * blockSize E (adaptedMean P (roundedGrid l mAl) ↑(Prop42Scalar.correctedTiltScale n₀ mOut)) ≤ 1 ∧ 9 / 2 * (c * blockSize E (adaptedMean P (roundedGrid l mAl) ↑(Prop42Scalar.correctedTiltScale n₀ mOut))) ≤ 9 / 2 * A * Real.rpow 3 (-↑(mOut - Prop42Scalar.correctedTiltScale n₀ mOut))

The corrected-tilt transfer inputs. At the corrected halfway scale the reverse Euclidean adapter supplies the Loewner comparison together with the unit cap on the absorbed size and the decaying error clause, in the exact shapes the corrected tilt transfer consumes. The hatted unit cap and the hatted tail are the two remaining inputs; the first is the bootstrap smallness at tolerance one, the second is the recursion's decay.