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

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

Scale-zero Caccioppoli budget envelopes

This file contains the dimension-only budget envelopes and explicit scale-zero bridge constants used by the scalar Caccioppoli envelope.

Audit tag

Claim: bound all unit-scale boundary and centered-interior alpha/cross/local budgets by dimension-only envelopes.

Downstream target: CoarseCaccioppoliScaleZeroScalarBounds.lean. This file should contain scalar envelope arithmetic only, not public package constructors.

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

Dimension-only cross/local budget envelope for the scale-zero boundary local-patch route.

Equations

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

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

Dimension-only cross/local budget envelope for the scale-zero centered interior route.

Equations

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

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

Dimension-dependent envelope for the centered average front, including the cutoff gradient factor.

Equations

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

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

Dimension-dependent envelope for the centered Hessian front, including the cutoff Hessian factor.

Equations

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

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

Dimension-dependent envelope for the centered gradient front, including the cutoff gradient factor.

Equations

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

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

Boundary scale-zero alpha budget envelope formed from the three centered fronts and bounded below by one.

Equations

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

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

Interior scale-zero alpha budget envelope formed from the three centered fronts and bounded below by one.

Equations

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

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

Boundary scale-zero alpha budget envelope multiplied by the number of spatial coordinates.

Equations

• HCPolySupport.Book.Ch03.boundaryScaleZeroAlphaInternalEnvelope d = ↑(Fintype.card (Fin d)) * HCPolySupport.Book.Ch03.boundaryScaleZeroAlphaBudgetEnvelope d

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

Interior scale-zero alpha budget envelope multiplied by the number of spatial coordinates.

Equations

• HCPolySupport.Book.Ch03.interiorScaleZeroAlphaInternalEnvelope d = ↑(Fintype.card (Fin d)) * HCPolySupport.Book.Ch03.interiorScaleZeroAlphaBudgetEnvelope d

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

Boundary scale-zero cross budget envelope multiplied by the number of spatial coordinates.

Equations

• HCPolySupport.Book.Ch03.boundaryScaleZeroCrossInternalEnvelope d = ↑(Fintype.card (Fin d)) * HCPolySupport.Book.Ch03.boundaryScaleZeroCrossBudgetEnvelope d

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

Interior scale-zero cross budget envelope multiplied by the number of spatial coordinates.

Equations

• HCPolySupport.Book.Ch03.interiorScaleZeroCrossInternalEnvelope d = ↑(Fintype.card (Fin d)) * HCPolySupport.Book.Ch03.interiorScaleZeroCrossBudgetEnvelope d

noncomputable def HCPolySupport.Book.Ch03.boundaryCaccioppoliScaleZeroExplicitConstant (d : ℕ) (s t : ℝ) : ℝ

Explicit scale-zero boundary constant produced by the completed deterministic Caccioppoli bridge with the standard beta-dependent radius iteration. This still depends on the exponents s,t; the remaining scalar majorization step is to bound it by one dimension-only constant on 0 < s, 0 < t, s + t < 1.

Equations

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

noncomputable def HCPolySupport.Book.Ch03.interiorCaccioppoliScaleZeroExplicitConstant (d : ℕ) (s t : ℝ) : ℝ

Explicit scale-zero centered-interior constant produced by the completed split deterministic Caccioppoli bridge with the standard beta-dependent radius iteration.

Equations

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

theorem HCPolySupport.Book.Ch03.boundaryCaccioppoliScaleZeroExplicitConstant_le_envelopeExplicit {d : ℕ} {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : boundaryCaccioppoliScaleZeroExplicitConstant d s t ≤ 18 ^ d * caccioppoliStandardExplicitNoteBoundSplit s t (boundaryScaleZeroAlphaInternalEnvelope d * s⁻¹) (boundaryScaleZeroCrossInternalEnvelope d)

theorem HCPolySupport.Book.Ch03.interiorCaccioppoliScaleZeroExplicitConstant_le_envelopeExplicit {d : ℕ} {s t : ℝ} (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) : interiorCaccioppoliScaleZeroExplicitConstant d s t ≤ 18 ^ d * caccioppoliStandardExplicitNoteBoundSplit s t (interiorScaleZeroAlphaInternalEnvelope d * s⁻¹) (interiorScaleZeroCrossInternalEnvelope d)