Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section4.Support.AffineExcess

AffineExcess #

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The affine excess E(u,W) and the best-affine slope #

ABK26, Β§4.3 opens with two displays. With 𝕃 the affine functions on ℝ^d,

E(u,W) := |W|^{-1/d} min_{β„“ ∈ 𝕃} β€–u βˆ’ β„“β€–_{LΒ²(W)},   β„“(u,W) := argmin_{β„“ ∈ 𝕃} …   (e.excess.def)
E(u,β–‘_m) := 3^{-m} min_{β„“ ∈ 𝕃} β€–u βˆ’ β„“β€–_{LΒ²(β–‘_m)}                              (e.excess.def.cubes)

Both normalizers are consumed downstream --- the iteration lemma runs E_j at the |U_j|^{-1/d} normalizer on truncated windows, while the Β§4.4 setup and the reabsorption constant read E_j at 3^{-j}. This module defines both normalizations and records the volume estimates used by their downstream comparisons on sandwiched windows.

Naming #

The identifier excess is already taken in this repository: cgExcess and its relatives are the Β§4.2 coarse-grained ellipticity excess (σλ^{-1} βˆ’ C_cg)β‚Š, an unrelated object. Everything here is therefore named affineExcess… / affineMinimizer…, and no declaration in this tree is called excess.

Attainment, honestly #

The source writes min and argmin and never argues attainment. This module defines the excess by sInf over the affine parameter space, which is unconditional and agrees with the source wherever the minimum exists, and supplies

Attainment itself is a separate theorem in Section4/Provider/ExcessDecay/AffineMinimizerExistence.lean, with its hypotheses visible. No uniqueness statement is claimed anywhere: the source's argmin notation is not backed by an argument, and none of the Β§4.3 estimates needs one.

Scope #

Like Section4/Support/Dirichlet.lean, this module serves frozen statements and is importable anywhere in the Section-4 tree.

References #

Affine functions and the affine distance #

source
def Algsuperdiff.Section4.Support.affineEval {d : β„•} (c : ℝ) (g x : HCPolySupport.Vec d) :
ℝ

The affine function x ↦ c + g Β· x with intercept c and slope g = βˆ‡β„“.

Equations
Instances For
    source
    theorem Algsuperdiff.Section4.Support.affineEval_sub {d : β„•} (c c' : ℝ) (g g' x : HCPolySupport.Vec d) :
    affineEval c g x - affineEval c' g' x = affineEval (c - c') (g - g') x

    The difference of two affine functions is affine in the parameter difference.

    source
    theorem Algsuperdiff.Section4.Support.affineEval_zero {d : β„•} (x : HCPolySupport.Vec d) :
    affineEval 0 0 x = 0
    source
    noncomputable def Algsuperdiff.Section4.Support.affineDistOn {d : β„•} (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d β†’ ℝ) (c : ℝ) (g : HCPolySupport.Vec d) :
    ℝ

    β€–u βˆ’ β„“β€–_{LΒ²(W)} for the affine function β„“ = (c, g).

    Equations
    Instances For
      source
      theorem Algsuperdiff.Section4.Support.affineDistOn_nonneg {d : β„•} (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d β†’ ℝ) (c : ℝ) (g : HCPolySupport.Vec d) :
      0 ≀ affineDistOn W u c g

      The excess as an infimum over affine competitors #

      source
      def Algsuperdiff.Section4.Support.affineDistSet {d : β„•} (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d β†’ ℝ) :
      Set ℝ

      The competitor set {β€–u βˆ’ β„“β€–_{LΒ²(W)} : β„“ ∈ 𝕃}, indexed by the parameter pair (c, g) ∈ ℝ Γ— Vec d.

      Equations
      Instances For
        source
        theorem Algsuperdiff.Section4.Support.affineDistSet_nonneg {d : β„•} (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d β†’ ℝ) (y : ℝ) :
        y ∈ affineDistSet W u β†’ 0 ≀ y
        source
        theorem Algsuperdiff.Section4.Support.affineDistSet_bddBelow {d : β„•} (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d β†’ ℝ) :
        BddBelow (affineDistSet W u)
        source
        theorem Algsuperdiff.Section4.Support.affineDistSet_nonempty {d : β„•} (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d β†’ ℝ) :
        (affineDistSet W u).Nonempty
        source
        noncomputable def Algsuperdiff.Section4.Support.affineExcessRaw {d : β„•} (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d β†’ ℝ) :
        ℝ

        The unnormalized excess min_{β„“ ∈ 𝕃} β€–u βˆ’ β„“β€–_{LΒ²(W)}, taken as an infimum.

        Equations
        Instances For
          source
          noncomputable def Algsuperdiff.Section4.Support.affineExcess {d : β„•} (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d β†’ ℝ) :
          ℝ

          The excess E(u,W) = |W|^{-1/d} min_{β„“ ∈ 𝕃} β€–u βˆ’ β„“β€–_{LΒ²(W)} of e.excess.def.

          Equations
          Instances For
            source
            noncomputable def Algsuperdiff.Section4.Support.affineExcessScaled {d : β„•} (j : β„€) (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d β†’ ℝ) :
            ℝ

            The scale-normalized excess 3^{-j} min_{β„“ ∈ 𝕃} β€–u βˆ’ β„“β€–_{LΒ²(W)}: the normalizer of e.excess.def.cubes, read on an arbitrary window at the declared scale j. On W = β–‘_j it agrees with affineExcess (affineExcess_openCubeSet).

            Equations
            Instances For
              source
              theorem Algsuperdiff.Section4.Support.affineExcessRaw_nonneg {d : β„•} (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d β†’ ℝ) :
              0 ≀ affineExcessRaw W u
              source
              theorem Algsuperdiff.Section4.Support.affineExcess_nonneg {d : β„•} (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d β†’ ℝ) :
              0 ≀ affineExcess W u
              source
              theorem Algsuperdiff.Section4.Support.affineExcessRaw_le_affineDistOn {d : β„•} (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d β†’ ℝ) (c : ℝ) (g : HCPolySupport.Vec d) :
              affineExcessRaw W u ≀ affineDistOn W u c g

              The projection inequality. The excess minimum is at most the distance to any affine competitor. This is the ≀-half of the source's min, and it is the inequality every excess estimate is read off against.

              source
              theorem Algsuperdiff.Section4.Support.affineExcessRaw_le_normalizedL2On_sub_const {d : β„•} (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d β†’ ℝ) (c : ℝ) :
              affineExcessRaw W u ≀ normalizedL2On W fun (x : HCPolySupport.Vec d) => u x - c

              The zero-slope competitor: the excess is at most the deviation of u from any constant.

              The best-affine map β„“(u,W) and its slope #

              source
              def Algsuperdiff.Section4.Support.IsAffineMinimizer {d : β„•} (W : Set (HCPolySupport.Vec d)) (u : HCPolySupport.Vec d β†’ ℝ) (c : ℝ) (g : HCPolySupport.Vec d) :
              Prop

              (c, g) attains the excess minimum: the source's β„“(u,W) = argmin, as a property of a parameter pair. No uniqueness is claimed.

              Equations
              Instances For
                source
                noncomputable def Algsuperdiff.Section4.Support.slopeMagnitude {d : β„•} (g : HCPolySupport.Vec d) :
                ℝ

                The euclidean slope magnitude |βˆ‡β„“| = β€–gβ€–β‚‚: the quantity p_j = |βˆ‡β„“(u,U_j)| of the iteration lemma.

                Equations
                Instances For
                  source
                  theorem Algsuperdiff.Section4.Support.slopeMagnitude_nonneg {d : β„•} (g : HCPolySupport.Vec d) :
                  0 ≀ slopeMagnitude g

                  The two normalizers #

                  source
                  theorem Algsuperdiff.Section4.Support.affineExcess_openCubeSet {d : β„•} (hd : d β‰  0) (Q : HCPolySupport.TriadicCube d) (u : HCPolySupport.Vec d β†’ ℝ) :
                  affineExcess (HCPolySupport.openCubeSet Q) u = affineExcessScaled Q.scale (HCPolySupport.openCubeSet Q) u

                  e.excess.def.cubes. On the triadic cube β–‘_m the general normalizer |W|^{-1/d} is the cube normalizer 3^{-m}; the two displays agree there. This is the whole content of the specialization.

                  source
                  theorem Algsuperdiff.Section4.Support.rpow_normalizer_bounds {d : β„•} (hd : d β‰  0) {V : ℝ} {j : β„€} (hlo : (3 ^ (j - 2)) ^ d ≀ V) (hhi : V ≀ (3 ^ j) ^ d) :
                  3 ^ (-j) ≀ V ^ (-(↑d)⁻¹) ∧ V ^ (-(↑d)⁻¹) ≀ 9 * 3 ^ (-j)

                  The normalizer comparison on a window whose volume is sandwiched between the volumes of the triadic cubes at scales j-2 and j --- the aspect ratio 3^{-2} pinned by the source (: the sharper ratio 1/2 available for the paper's own truncated windows is not used; constants stay at the printed 3^{-2}).