Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Fractional.ExactOverlapEuclideanLpDisjointBridge

Coarse-graining support: Support.Sobolev.Fractional.ExactOverlapEuclideanLpDisjointBridge #

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

Disjoint-to-exact-overlap finite-p bridge #

This file keeps the only localization step needed by the finite-p coarse-graining forcing argument in the disjoint lane. It compares the resulting parent disjoint series to the canonical exact overlap series; it does not assert localization of the overlap seminorm itself.

source
noncomputable def HCPolySupport.cubeEuclideanPositiveBesovDisjointDepthPower {d : ℕ} (Q : TriadicCube d) (p : FiniteLpExponent) (F : Vec d → Vec d) (j : ℕ) :
ENNReal

The unrooted Euclidean oscillation average over ordinary triadic descendants at one depth.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.cubeEuclideanPositiveBesovDisjointPowerEnergy {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) :
    ENNReal

    The literal running-scale disjoint positive-Besov power series used only internally before the parent overlap bridge.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.cubeEuclideanPositiveBesovDisjointDepthPower_le_overlap {d : ℕ} (Q : TriadicCube d) (p : FiniteLpExponent) (F : Vec d → Vec d) (j : ℕ) :
      cubeEuclideanPositiveBesovDisjointDepthPower Q p F j ≤ 3 ^ d * cubeEuclideanPositiveBesovOverlapDepthENorm Q p F j ^ p.exponent.toReal

      At a fixed depth, the ordinary disjoint Euclidean oscillation average is controlled by the exact overlap average. The only loss is the dimension-only middle-child cardinality factor.

      source
      theorem HCPolySupport.cubeEuclideanPositiveBesovDisjointPowerEnergy_le_overlap {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : Vec d → Vec d) :
      cubeEuclideanPositiveBesovDisjointPowerEnergy Q s p F ≤ 3 ^ d * cubeEuclideanPositiveBesovOverlapPowerEnergy Q s p F

      The complete disjoint forcing power series is controlled by the literal parent overlap power energy with a dimension-only factor.

      source
      theorem HCPolySupport.cubeEuclideanPositiveBesovDisjointPowerEnergy_root_le_overlap {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (hp : 2 ≤ p.exponent) (F : Vec d → Vec d) :
      cubeEuclideanPositiveBesovDisjointPowerEnergy Q s p F ^ p.exponent.toReal⁻¹ ≤ 3 ^ d * cubeEuclideanPositiveBesovOverlapESeminorm Q s p F

      For p ≥ 2, rooting the disjoint forcing power energy preserves a dimension-only bridge constant.