Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch01.Theorems.CubeNeumannCZ

Coarse-graining support: Support.Book.Ch01.Theorems.CubeNeumannCZ #

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

Legacy Chapter 1 Neumann compatibility facade #

This module is deliberately quarantined in HCPolySupport.Book.Ch01.Legacy. Its selected constant and regularity theorem alias a downstream positive-test estimate; they are not the literal weak-Hessian Calderon--Zygmund statement from the manuscript.

source
@[reducible, inline]
noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.cubeNeumannW22Constant (d : ℕ) :
ℝ

Legacy selected constant for the downstream Neumann positive-test compatibility package on cubes.

Equations
Instances For
    source
    theorem HCPolySupport.Book.Ch01.Legacy.cubeNeumannW22Constant_nonneg (d : ℕ) :
    0 ≤ cubeNeumannW22Constant d
    source
    theorem HCPolySupport.Book.Ch01.Legacy.cubeNeumannW22Regularity {d : ℕ} (Q : Cube d) :
    Legacy.CubeNeumannW22CalderonZygmundRegularity Q (cubeNeumannW22Constant d)

    Legacy cube Neumann positive-test compatibility theorem. This is not the literal weak-Hessian Calderon--Zygmund theorem.

    source
    theorem HCPolySupport.Book.Ch01.Legacy.exists_cubeNeumannW22RegularityInDimension (d : ℕ) :
    ∃ (C : ℝ), Legacy.CubeNeumannW22CalderonZygmundRegularityInDimension d C

    Dimension-uniform existence form of the legacy cube Neumann positive-test compatibility package.