Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubePoisson.EndpointDuality

Coarse-graining support: Support.Sobolev.Foundations.CubePoisson.EndpointDuality #

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

Endpoint Besov-duality interfaces for Poisson-gradient pairings #

The endpoint Besov duality definitions used by the cube-local Poincare arguments, together with the conversions between projected and full-dual surfaces. The to_l2Endpoint and of_dualTestNorm… lemmas wire these surfaces to the Calderon-Zygmund and dual-test-norm estimates from sibling files.

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

Endpoint Besov duality input, specialized to the projected gradient terms that occur in the one-cube vector Poincare proof.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def HCPolySupport.CubeGradientEndpointDuality {d : ℕ} (Q : TriadicCube d) (C : ℝ) :
    Prop

    Endpoint Besov duality input for the full, unprojected gradient terms used by the infinite-depth vector Poincare theorem.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def HCPolySupport.CubePoissonGradientFullEndpointDuality {d : ℕ} (Q : TriadicCube d) (C : ℝ) :
      Prop

      Constant-mode-safe endpoint Besov duality input for the Poisson-gradient test fields that occur in the infinite-depth vector Poincare proof.

      This is the corrected replacement surface for arbitrary H¹ inputs: the first factor is measured by the full dual norm, so constant gradient modes are not discarded.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def HCPolySupport.CubePoissonGradientFullL2EndpointDuality {d : ℕ} (Q : TriadicCube d) (C : ℝ) :
        Prop

        L²-facing full-dual endpoint Besov duality input for Poisson-gradient test fields.

        This packages the combination of full-dual scalar pairing and positive test-norm control after the Neumann CZ estimate has already converted the Poisson-gradient side to the normalized L² size of the right-hand side.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem HCPolySupport.CubePoissonGradientFullEndpointDuality.to_l2Endpoint {d : ℕ} {Q : TriadicCube d} {Cdual Ccz : ℝ} (hdual : CubePoissonGradientFullEndpointDuality Q Cdual) (hcz : CubeNeumannPoissonGradientBesovEstimate Q Ccz) :
          CubePoissonGradientFullL2EndpointDuality Q (Cdual * Ccz)
          source
          theorem HCPolySupport.CubePoissonGradientFullEndpointDuality.of_dualTestNormEstimate {d : ℕ} {Q : TriadicCube d} {C : ℝ} (h : CubePoissonGradientDualTestNormEstimate Q C) :
          CubePoissonGradientFullEndpointDuality Q C
          source
          theorem HCPolySupport.CubePoissonGradientFullL2EndpointDuality.of_dualTestNormL2Estimate {d : ℕ} {Q : TriadicCube d} {C : ℝ} (h : CubePoissonGradientDualTestNormL2Estimate Q C) :
          CubePoissonGradientFullL2EndpointDuality Q C