Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubeNeumannW22CZ.Regularity

Coarse-graining support: Support.Sobolev.Foundations.CubeNeumannW22CZ.Regularity #

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

Legacy positive-test Neumann compatibility package #

This module packages the downstream positive-test endpoint for Neumann Poisson solutions. It does not state the manuscript's weak-Hessian Calderon--Zygmund estimate; that literal statement lives in the exact Euclidean-normalized lane.

source
def HCPolySupport.Legacy.CubeNeumannW22CalderonZygmundRegularity {d : ℕ} (Q : TriadicCube d) (C : ℝ) :
Prop

Legacy name for the downstream positive-test core estimate. This is a compatibility wrapper, not a weak-Hessian Calderon--Zygmund statement.

Equations
Instances For
    source
    def HCPolySupport.Legacy.CubeNeumannW22CalderonZygmundRegularityInDimension (d : ℕ) (C : ℝ) :
    Prop

    Dimension-uniform legacy positive-test compatibility predicate on cubes.

    Equations
    Instances For
      source
      noncomputable def HCPolySupport.Legacy.cubeNeumannW22CalderonZygmundConstant (d : ℕ) :
      ℝ

      Chosen dimension-only constant for the legacy positive-test compatibility package, obtained from the reflected-parent depth and component-average constants.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem HCPolySupport.Legacy.cubeNeumannW22CalderonZygmundConstant_nonneg (d : ℕ) :
        0 ≤ cubeNeumannW22CalderonZygmundConstant d
        source
        theorem HCPolySupport.Legacy.cubeNeumannW22CalderonZygmundRegularity {d : ℕ} (Q : TriadicCube d) :
        CubeNeumannW22CalderonZygmundRegularity Q (cubeNeumannW22CalderonZygmundConstant d)

        Selected legacy positive-test compatibility estimate on a cube.

        source
        theorem HCPolySupport.Legacy.exists_cubeNeumannW22CalderonZygmundRegularityInDimension (d : ℕ) :
        ∃ (C : ℝ), CubeNeumannW22CalderonZygmundRegularityInDimension d C

        The legacy positive-test compatibility package has the explicit constant above in every dimension.

        source
        theorem HCPolySupport.Legacy.exists_cubeNeumannW22CalderonZygmundRegularity {d : ℕ} (Q : TriadicCube d) :
        ∃ (C : ℝ), CubeNeumannW22CalderonZygmundRegularity Q C

        Local existence form of the legacy positive-test compatibility input.

        source
        theorem HCPolySupport.Legacy.exists_cubePoissonGradientDualTestNormL2CoreEstimate {d : ℕ} (Q : TriadicCube d) :
        ∃ (C : ℝ), CubePoissonGradientDualTestNormL2CoreEstimate Q C

        Downstream positive-test core estimate from the legacy compatibility package.