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

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

Scale-zero Caccioppoli scalar bounds

This file bounds the boundary and interior scale-zero explicit constants by one dimension-only scalar bound.

Audit tag

Claim: package the boundary and centered-interior explicit scale-zero constants under one dimension-only scalar bound.

Downstream target: CoarseCaccioppoliScaleZero.lean. This file should stay as the scalar-bound endpoint for the scale-zero stack.

noncomputable def HCPolySupport.Book.Ch03.caccioppoliScaleZeroEnvelopeBound (A X : ℝ) : ℝ

Scalar scale-zero envelope combining the alpha budget with the square of the cross budget.

Equations

• HCPolySupport.Book.Ch03.caccioppoliScaleZeroEnvelopeBound A X = 36 * (6561 * 6561 * X ^ 2) + 36 * Real.exp 1 * (9 * 4 * 81 * X * X * A) + 1

noncomputable def HCPolySupport.Book.Ch03.boundaryCaccioppoliScaleZeroScalarBound (d : ℕ) : ℝ

Boundary scale-zero scalar bound obtained from the internal alpha and cross envelopes with factor 18 to the dimension.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.interiorCaccioppoliScaleZeroScalarBound (d : ℕ) : ℝ

Interior scale-zero scalar bound obtained from the internal alpha and cross envelopes with factor 18 to the dimension.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.Book.Ch03.caccioppoliScaleZeroScalarBound (d : ℕ) : ℝ

A dimension-only scalar bound dominating both scale-zero bridge constants.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Book.Ch03.boundaryCaccioppoliScaleZeroExplicitConstant_le_scalarBound {d : ℕ} [NeZero d] {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : boundaryCaccioppoliScaleZeroExplicitConstant d s t ≤ boundaryCaccioppoliScaleZeroScalarBound d

theorem HCPolySupport.Book.Ch03.interiorCaccioppoliScaleZeroExplicitConstant_le_scalarBound {d : ℕ} [NeZero d] {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : interiorCaccioppoliScaleZeroExplicitConstant d s t ≤ interiorCaccioppoliScaleZeroScalarBound d