Coarse-graining support: Support.Book.Ch03.Theorems.CoarseCaccioppoliScalarEnvelopes

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Scalar envelopes for coarse Caccioppoli

This file contains the final scalar-envelope package used to upgrade scale-zero explicit constants to the note-facing dimension-only constant.

structure HCPolySupport.Book.Ch03.CoarseCaccioppoliScaleZeroScalarEnvelope (d : ℕ) [NeZero d] : Prop

Scalar envelope needed to upgrade the scale-zero explicit bridge constants to the note-facing dimension-only C(d). This is deliberately only a scalar statement: all PDE and geometry work has already been discharged below this surface.

• exists_constant : ∃ (C : ℝ), 0 < C ∧ (∀ {s t : ℝ}, 0 < s → 0 < t → s + t < 1 → boundaryCaccioppoliScaleZeroExplicitConstant d s t ≤ C) ∧ ∀ {s t : ℝ}, 0 < s → 0 < t → s + t < 1 → interiorCaccioppoliScaleZeroExplicitConstant d s t ≤ C

theorem HCPolySupport.Book.Ch03.coarseCaccioppoliScaleZeroScalarEnvelope (d : ℕ) [NeZero d] : CoarseCaccioppoliScaleZeroScalarEnvelope d

The scale-zero scalar envelope is fully proved from the explicit split s,t bookkeeping.