High-contrast homogenization: Provider.Quenched.SmallContrastBootstrapFiniteBandTransfer

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

The corrected-tilt transfer across its finite adapter band

The raw reverse-adapter construction has a unit-size premise. Its law factor is paid by the endpoint's linear level-schedule start, so that premise is available once the corrected scale gap reaches the corresponding finite band. Before that band, monotonicity and the entry floor imply the endpoint transfer directly: the endpoint prefactor times the triadic decay is at least one there.

theorem HCPolySupport.HighContrast.Quenched.adapter_factor_le_at_finite_band {rate adapter : ℝ} {nF R : ℕ} (hrate : 0 ≤ rate) (hnF : nF ≤ R) (hadapter : adapter ≤ Real.rpow 3 (rate * ↑nF)) : adapter ≤ Real.rpow 3 (rate * ↑R)

A reverse-adapter factor paid at generation nF is still paid at every later generation R.

theorem HCPolySupport.HighContrast.Quenched.finite_band_adapter_size_le_one {rate : ℝ} {R gap : ℕ} (hlate : rate * ↑R ≤ ↑gap) : Real.rpow 3 (rate * ↑R) * Real.rpow 3 (-↑gap) ≤ 1

Once the scale gap reaches the delay exponent, the raw construction's absorbed size coefficient is at most one.

theorem HCPolySupport.HighContrast.Quenched.one_le_finite_band_transfer_decay {rate floor0 : ℝ} {R gap : ℕ} (hfloor0 : 0 ≤ floor0) (hearly : ↑gap < rate * ↑R) : 1 ≤ (1 + floor0) * Real.rpow 3 (rate * ↑R) * Real.rpow 3 (-↑gap)

Before the adapter delay, the endpoint coefficient cancels the triadic decay and leaves at least the a-priori unit floor.

theorem HCPolySupport.HighContrast.Quenched.one_le_finite_band_transfer_prefactor {rate floor0 : ℝ} {R : ℕ} (hrate : 0 ≤ rate) (hfloor0 : 0 ≤ floor0) : 1 ≤ 9 / 2 * ((1 + floor0) * Real.rpow 3 (rate * ↑R))

The endpoint coefficient is at least one already at the boundary scale.

theorem HCPolySupport.HighContrast.Quenched.outer_transfer_of_corrected_tilt_inputs_of_finite_band {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P g E Ψ K S) {l : ℤ} {q : Mat d} (hq : IsRoundedGrid l q) (hfin : ∀ (k : ℤ), HasFiniteAdaptedMean P q k) {n₀ nF R : ℕ} {cStar rate floor0 adapter : ℝ} (hentry : annealedContrast P 0 - 1 ≤ cStar) (hcStar1 : cStar ≤ 1) (hrate : 0 ≤ rate) (hfloor0 : 0 ≤ floor0) (hnF : nF ≤ R) (hadapter : adapter ≤ Real.rpow 3 (rate * ↑nF)) (hpack : ∀ (m : ℕ), 2 * n₀ < m → ∀ (A : ℝ), adapter ≤ A → A * Real.rpow 3 (-↑(m - Prop42Scalar.correctedTiltScale n₀ m)) ≤ 1 → ∃ (c : ℝ), 0 ≤ c ∧ BlockMatLoewnerLE (blockSub (annealedBlock P (centeredCube d ↑m)) (adaptedMean P q ↑(Prop42Scalar.correctedTiltScale n₀ m))) (blockScale c E) ∧ c * blockSize E (adaptedMean P q ↑(Prop42Scalar.correctedTiltScale n₀ m)) ≤ 1 ∧ 9 / 2 * (c * blockSize E (adaptedMean P q ↑(Prop42Scalar.correctedTiltScale n₀ m))) ≤ 9 / 2 * A * Real.rpow 3 (-↑(m - Prop42Scalar.correctedTiltScale n₀ m))) (hx1 : ∀ (m : ℕ), 2 * n₀ < m → ↑d * (adaptedHattedContrast P q ↑(Prop42Scalar.correctedTiltScale n₀ m) - 1) ≤ 1) (m : ℕ) : 2 * n₀ ≤ m → annealedContrast P ↑m - 1 ≤ 9 / 2 * (↑d * (adaptedHattedContrast P q ↑(Prop42Scalar.correctedTiltScale n₀ m) - 1)) + 9 / 2 * ((1 + floor0) * Real.rpow 3 (rate * ↑R)) * Real.rpow 3 (-↑(m - Prop42Scalar.correctedTiltScale n₀ m))

The corrected outer transfer with a finite adapter band. Entry smallness handles the boundary, the a-priori floor handles the finite band, and the raw corrected-tilt construction handles every later generation.