Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.CubePoisson.BesovEstimate

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

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

Calderon-Zygmund Besov gradient estimate for the cube Poisson solver #

The narrow Calderon-Zygmund consequence used by the projected vector Poincare proof: the gradient of the Neumann Poisson solution has controlled positive B¹_{2,∞} circ norm, component by component, with the constant produced from the coercive H¹ bound and a geometric Besov scale weight.

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

The narrow Calderon-Zygmund consequence needed for the projected vector Poincare proof: the gradient of the Neumann Poisson solution has controlled positive B¹_{2,∞} circ norm, component by component.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.sum_cubeBesovCircNorm_one_two_top_le_geometric_mul_sum_cubeLpNorm {d : ℕ} (Q : TriadicCube d) (G : Vec d → Vec d) (hG : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => G x i) 2 (normalizedCubeMeasure Q)) :
    (∑ i : Fin d, cubeBesovCircNorm Q 1 2 ⊤ fun (x : Vec d) => G x i) ≤ cubeBesovScaleWeight (-1) Q * (1 - 3 ^ (-1))⁻¹ * ∑ i : Fin d, cubeLpNorm Q 2 fun (x : Vec d) => G x i

    Componentwise geometric control of the positive B¹_{2,∞} circ norm by normalized component L² norms. This is the Besov side of the narrow Calderon-Zygmund dependency; the remaining elliptic part is to control the Poisson-gradient component L² sum by the right-hand side.

    source
    noncomputable def HCPolySupport.cubeNeumannPoissonGradientBesovEnergyConstant {d : ℕ} (Q : TriadicCube d) :
    ℝ

    The explicit Poisson-gradient Besov bound obtained by multiplying the geometric Besov factor by the cube energy and coercivity factors.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.cubeNeumannPoissonGradientBesovEnergyConstant_nonneg {d : ℕ} (Q : TriadicCube d) :
      0 ≤ cubeNeumannPoissonGradientBesovEnergyConstant Q
      source
      theorem HCPolySupport.cubeNeumannPoissonGradientBesovEstimate_of_energy {d : ℕ} (Q : TriadicCube d) :
      CubeNeumannPoissonGradientBesovEstimate Q (cubeNeumannPoissonGradientBesovEnergyConstant Q)