Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch01.Theorems.MultiscalePoincare

Coarse-graining support: Support.Book.Ch01.Theorems.MultiscalePoincare #

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

Legacy disjoint-Besov multiscale Poincare compatibility lane #

The declarations in this namespace are retained only for compatibility with the legacy disjoint-positive, totalized-real, componentwise-circ Besov conventions. They are not the exact manuscript overlap/Euclidean statements.

source
@[reducible, inline]
noncomputable abbrev HCPolySupport.Book.Ch01.Legacy.fullVectorPoincareConstant {d : ℕ} (Q : Cube d) :
ℝ

Legacy selected constant for the disjoint-positive, totalized-real, componentwise-circ compatibility Poincare lane; not an exact manuscript overlap/Euclidean constant.

Equations
Instances For
    source
    theorem HCPolySupport.Book.Ch01.Legacy.fullVectorPoincareConstant_nonneg {d : ℕ} (Q : Cube d) :
    0 ≤ fullVectorPoincareConstant Q
    source
    theorem HCPolySupport.Book.Ch01.Legacy.h1_fullVectorPoincare {d : ℕ} (Q : Cube d) (u : H1Function (openCubeSet Q)) :
    CubeDualFullVectorPoincareEstimate Q (fullVectorPoincareConstant Q) (fun (x : HCPolySupport.Vec d) => u.toFun x) fun (x : HCPolySupport.Vec d) => u.grad x

    Legacy full-dual multiscale Poincare compatibility estimate for H¹ functions on cubes; not an exact manuscript overlap/Euclidean statement.

    source
    theorem HCPolySupport.Book.Ch01.Legacy.h1_descendantFullVectorPoincare {d : ℕ} (Q : Cube d) (u : H1Function (openCubeSet Q)) (N : ℕ) :
    CubeDescendantDualFullVectorPoincareEstimate Q (fullVectorPoincareConstant Q) (cubeFluctuation Q fun (x : HCPolySupport.Vec d) => u.toFun x) (fun (x : HCPolySupport.Vec d) => u.grad x) N

    Legacy descendant full-dual Poincare compatibility estimate for H¹ functions on cubes; not an exact manuscript overlap/Euclidean statement.

    source
    theorem HCPolySupport.Book.Ch01.Legacy.h1_descendantLocalFullCircPoincare {d : ℕ} (Q : Cube d) (u : H1Function (openCubeSet Q)) (N : ℕ) :
    CubeLocalFullCircPoincareVectorEstimate Q (fullVectorPoincareConstant Q * 3 ^ (↑d + 1)) (cubeFluctuation Q fun (x : HCPolySupport.Vec d) => u.toFun x) (fun (x : HCPolySupport.Vec d) => u.grad x) N

    Legacy descendant H1 Poincare compatibility estimate after componentwise circ domination. This is not an exact manuscript overlap/Euclidean statement.

    This is the honest full-circ bridge available from the full-dual theorem. The remaining gradient-to-function cleanup is the separate summation step from local full-circ control to the finite-partial multiscale corridor, or an equivalent direct infinite-depth summation theorem.

    source
    theorem HCPolySupport.Book.Ch01.Legacy.h1_fluctuation_partialNormTop_two_le_sum_grad_circNorm {d : ℕ} (Q : Cube d) (s : ℝ) (M : ℕ) (u : H1Function (openCubeSet Q)) (hs0 : 0 < s) (hs1 : s < 1) :
    cubeBesovPartialNormTop Q s 2 M (cubeFluctuation Q fun (x : HCPolySupport.Vec d) => u.toFun x) ≤ fullVectorPoincareConstant Q * 3 ^ (↑d + 1) * ∑ i : Fin d, circNegativeBesovNorm Q (1 - s) 2 1 fun (x : Vec d) => u.grad x i

    Legacy finite-depth, disjoint-positive/totalized-real, componentwise-circ multiscale Poincare compatibility estimate; not an exact manuscript overlap/Euclidean statement.