Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch03.Theorems.HomogenizationBlackBoxes

Coarse-graining support: Support.Book.Ch03.Theorems.HomogenizationBlackBoxes #

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

Section 3.3: Deterministic homogenization black boxes #

This file bundles the public contract packages for all currently written theorems in Chapter 3.3.

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

Public aggregate package for the proved two-exponent replacement route.

This is the downstream-facing Ch3.3 surface when the comparison left-hand side is measured at exponent s, but the flux-defect/Besov input is consumed at an independent exponent t < s / 2 with the explicit note-facing singular factor in the public RHS.

Instances For
    source
    theorem HCPolySupport.Book.Ch03.homogenizationBlackBoxesTheory (d : ℕ) [NeZero d] :
    HomogenizationBlackBoxesTheory d

    Public Chapter 3.3 two-exponent black-box package with all currently formalized analytic inputs discharged.