Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubeCalderonZygmund.H10Adjoint

Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.H10Adjoint #

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

Zero-trace scalar divergence solutions on cubes #

This file packages the existing Riesz/Dirichlet construction as a canonical zero-trace solution of a scalar constant-coefficient divergence equation. Its weak equation has the negative-divergence sign used by finite-q comparisons.

source
theorem HCPolySupport.CubeCalderonZygmund.exists_axisCubeScalarDivergenceSolution {d : ℕ} [NeZero d] (z : Vec d) {L sigma0 : ℝ} (hL : 0 < L) (hsigma0 : 0 < sigma0) (G : Vec d → Vec d) (hG : MemVectorL2 (axisCube z L) G) :
∃ (v : H10Function (axisCube z L)), (∀ (ψ : H10Function (axisCube z L)), sigma0 * ∫ (x : Vec d) in axisCube z L, vecDot (v.grad x) (ψ.grad x) = -∫ (x : Vec d) in axisCube z L, vecDot (G x) (ψ.grad x)) ∧ ‖v.gradToHilbertVectorL2‖ ≤ sigma0⁻¹ * ‖toHilbertVectorL2OfVecField hG‖

A zero-trace solution of the scalar constant-coefficient divergence equation on an open axis cube, with its sharp Hilbert-vector energy estimate.

source
noncomputable def HCPolySupport.CubeCalderonZygmund.axisCubeScalarDivergenceSolution {d : ℕ} [NeZero d] (z : Vec d) {L sigma0 : ℝ} (hL : 0 < L) (hsigma0 : 0 < sigma0) (G : Vec d → Vec d) (hG : MemVectorL2 (axisCube z L) G) :
H10Function (axisCube z L)

The canonical zero-trace solution of the scalar constant-coefficient divergence equation on an open axis cube.

Equations
Instances For
    source
    theorem HCPolySupport.CubeCalderonZygmund.axisCubeScalarDivergenceSolution_weak {d : ℕ} [NeZero d] (z : Vec d) {L sigma0 : ℝ} (hL : 0 < L) (hsigma0 : 0 < sigma0) (G : Vec d → Vec d) (hG : MemVectorL2 (axisCube z L) G) (ψ : H10Function (axisCube z L)) :
    sigma0 * ∫ (x : Vec d) in axisCube z L, vecDot ((axisCubeScalarDivergenceSolution z hL hsigma0 G hG).grad x) (ψ.grad x) = -∫ (x : Vec d) in axisCube z L, vecDot (G x) (ψ.grad x)

    The canonical axis-cube solution satisfies the scalar divergence equation against every zero-trace Sobolev test function.

    source
    theorem HCPolySupport.CubeCalderonZygmund.norm_axisCubeScalarDivergenceSolution_gradToHilbertVectorL2_le {d : ℕ} [NeZero d] (z : Vec d) {L sigma0 : ℝ} (hL : 0 < L) (hsigma0 : 0 < sigma0) (G : Vec d → Vec d) (hG : MemVectorL2 (axisCube z L) G) :
    ‖(axisCubeScalarDivergenceSolution z hL hsigma0 G hG).gradToHilbertVectorL2‖ ≤ sigma0⁻¹ * ‖toHilbertVectorL2OfVecField hG‖

    The canonical axis-cube solution has the sharp Hilbert-vector energy bound.

    source
    theorem HCPolySupport.CubeCalderonZygmund.exists_openCubeSetScalarDivergenceSolution {d : ℕ} [NeZero d] (Q : TriadicCube d) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (G : Vec d → Vec d) (hG : MemVectorL2 (openCubeSet Q) G) :
    ∃ (v : H10Function (openCubeSet Q)), (∀ (ψ : H10Function (openCubeSet Q)), sigma0 * ∫ (x : Vec d) in openCubeSet Q, vecDot (v.grad x) (ψ.grad x) = -∫ (x : Vec d) in openCubeSet Q, vecDot (G x) (ψ.grad x)) ∧ ‖v.gradToHilbertVectorL2‖ ≤ sigma0⁻¹ * ‖toHilbertVectorL2OfVecField hG‖

    Existence form on the open realization of a triadic cube. In particular this supplies the centered origin-cube interface used by the source-facing CZ estimates.

    source
    noncomputable def HCPolySupport.CubeCalderonZygmund.openCubeSetScalarDivergenceSolution {d : ℕ} [NeZero d] (Q : TriadicCube d) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (G : Vec d → Vec d) (hG : MemVectorL2 (openCubeSet Q) G) :
    H10Function (openCubeSet Q)

    The canonical scalar divergence solution on an open triadic cube.

    Equations
    Instances For
      source
      theorem HCPolySupport.CubeCalderonZygmund.openCubeSetScalarDivergenceSolution_weak {d : ℕ} [NeZero d] (Q : TriadicCube d) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (G : Vec d → Vec d) (hG : MemVectorL2 (openCubeSet Q) G) (ψ : H10Function (openCubeSet Q)) :
      sigma0 * ∫ (x : Vec d) in openCubeSet Q, vecDot ((openCubeSetScalarDivergenceSolution Q hsigma0 G hG).grad x) (ψ.grad x) = -∫ (x : Vec d) in openCubeSet Q, vecDot (G x) (ψ.grad x)

      The canonical open-triadic-cube solution satisfies the scalar divergence equation against every zero-trace Sobolev test function.

      source
      theorem HCPolySupport.CubeCalderonZygmund.norm_openCubeSetScalarDivergenceSolution_gradToHilbertVectorL2_le {d : ℕ} [NeZero d] (Q : TriadicCube d) {sigma0 : ℝ} (hsigma0 : 0 < sigma0) (G : Vec d → Vec d) (hG : MemVectorL2 (openCubeSet Q) G) :
      ‖(openCubeSetScalarDivergenceSolution Q hsigma0 G hG).gradToHilbertVectorL2‖ ≤ sigma0⁻¹ * ‖toHilbertVectorL2OfVecField hG‖

      The canonical open-triadic-cube solution has the sharp Hilbert-vector energy bound.