High-contrast homogenization: Annealed.ResponseBound

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

The almost sure entrywise bound on the coarse response

Under e.coarse.ellipticity the response on a centered cube is dominated by the reference block with a discount factor that the sample itself controls: run the assumption at the sample's own burn scale m' ≥ m, where 3^{m'} ≥ S, and pay the lost discount 3^{g(m'-m)}. Because the burn scale overshoots by at most one triadic step, that factor is affine in the source scale, and the entries of the response are bounded almost surely by an affine function of the source.

theorem HCPolySupport.HighContrast.exists_burn_scale (m : ℤ) (s : ℝ) : ∃ (m' : ℤ), m ≤ m' ∧ s ≤ 3 ^ m' ∧ 3 ^ m' ≤ 3 * max (3 ^ m) s

For every real s and every scale m there is a scale m' ≥ m at which the source has burned, s ≤ 3^{m'}, and which overshoots by at most one triadic step.

theorem HCPolySupport.HighContrast.ae_abs_blockMatEntry_coarseBlock_le {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {g : ℝ} {E : BlockMat d} {Ψ : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} (hdag : CoarseEllipticityDagger P g E Ψ K S) (m : ℤ) : ∀ᵐ (a : CoeffSpace d) ∂P, ∀ (α β : BlockCoord d), |blockMatEntry (coarseBlock (centeredCube d m) a) α β| ≤ 6 * blockEntrySum E * (1 + 3 ^ (-m) * S a)

The almost sure entrywise bound. Under e.coarse.ellipticity the entries of the coarse response on a centered cube are bounded, almost surely, by an affine function of the source scale.