Documentation

LeanPool.HighContrastHomogenization.Provider.Response.CutoffBasic

High-contrast homogenization: Provider.Response.CutoffBasic #

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The adapted pre-Young cutoff #

The cutoff is the normalized canonical product cutoff on the centered reference cube, pulled forward by the positive-definite grid matrix. Its chosen inner cube has at least half the parent volume, so normalization preserves the pointwise upper bound two.

source
noncomputable def HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff {d : ℕ} (q : Mat d) (_hq : Matrix.PosDef q) (t : ℤ) :
Vec d → ℝ

The smooth mean-one cutoff on the adapted cell.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_apply {d : ℕ} (q : Mat d) (hq : Matrix.PosDef q) (t : ℤ) (x : Vec d) :
    adaptedPreYoungCutoff q hq t x = (cubeAverage (originCube d t) (QuantitativeCubeCutoff.canonicalFun (originCube d t) (1 - 1 / (2 * ↑d)) (1 - 1 / (4 * ↑d))))⁻¹ * QuantitativeCubeCutoff.canonicalFun (originCube d t) (1 - 1 / (2 * ↑d)) (1 - 1 / (4 * ↑d)) (matVecMul q⁻¹ x)

    Defining equation for the adapted cutoff.

    source
    theorem HCPolySupport.HighContrast.Response.half_le_adaptedPreYoungCutoff_rawAverage {d : ℕ} [NeZero d] (t : ℤ) :
    1 / 2 ≤ cubeAverage (originCube d t) (QuantitativeCubeCutoff.canonicalFun (originCube d t) (1 - 1 / (2 * ↑d)) (1 - 1 / (4 * ↑d)))

    The unnormalized cutoff has average at least one half.

    source
    theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_rawAverage_pos {d : ℕ} [NeZero d] (t : ℤ) :
    0 < cubeAverage (originCube d t) (QuantitativeCubeCutoff.canonicalFun (originCube d t) (1 - 1 / (2 * ↑d)) (1 - 1 / (4 * ↑d)))

    The normalizing average is positive.

    source
    theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_inv_rawAverage_le_two {d : ℕ} [NeZero d] (t : ℤ) :
    (cubeAverage (originCube d t) (QuantitativeCubeCutoff.canonicalFun (originCube d t) (1 - 1 / (2 * ↑d)) (1 - 1 / (4 * ↑d))))⁻¹ ≤ 2

    Normalization enlarges the canonical cutoff by at most two.

    source
    theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_pullback_apply {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (y : Vec d) :
    adaptedPreYoungCutoff q hq t (matVecMul q y) = (cubeAverage (originCube d t) (QuantitativeCubeCutoff.canonicalFun (originCube d t) (1 - 1 / (2 * ↑d)) (1 - 1 / (4 * ↑d))))⁻¹ * QuantitativeCubeCutoff.canonicalFun (originCube d t) (1 - 1 / (2 * ↑d)) (1 - 1 / (4 * ↑d)) y

    Pulling the adapted cutoff back by its grid matrix recovers the normalized reference cutoff exactly.

    source
    theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_nonneg {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (x : Vec d) :
    0 ≤ adaptedPreYoungCutoff q hq t x

    The adapted cutoff is nonnegative.

    source
    theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_le_two {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (x : Vec d) :
    adaptedPreYoungCutoff q hq t x ≤ 2

    The normalized adapted cutoff is bounded above by two.

    source
    theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_smooth {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) :
    ContDiff ℝ (↑⊤) (adaptedPreYoungCutoff q hq t)

    The adapted cutoff is smooth.

    source
    theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_hasCompactSupport {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) :
    HasCompactSupport (adaptedPreYoungCutoff q hq t)

    The adapted cutoff has compact support.

    source
    theorem HCPolySupport.HighContrast.Response.adaptedPreYoungCutoff_tsupport_subset {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) :
    tsupport (adaptedPreYoungCutoff q hq t) ⊆ adaptedCell q t

    The compact support lies inside the open adapted cell.

    source
    theorem HCPolySupport.HighContrast.Response.cubeAverage_adaptedPreYoungCutoff_pullback_eq_one {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) :
    (cubeAverage (originCube d t) fun (y : Vec d) => adaptedPreYoungCutoff q hq t (matVecMul q y)) = 1

    The reference-cube average of the normalized pullback is one.