Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.FiniteLipschitzCoreDefinitions

High-contrast homogenization: Provider.Regularity.FiniteLipschitzCoreDefinitions #

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

Public finite centered-cube energy and best-fit objects #

This module exposes the finite centered-cube energy and canonical affine best-fit quantities used by both regularity branches.

source
noncomputable def HCPolySupport.HighContrast.finiteCenteredCubeSolutionEnergy {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) :
ℝ

The normalized energy of the solution restricted to a centered cube.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.HighContrast.finiteCenteredCubeSolutionEnergy_eq_of_le {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) (hkm : k ≤ m) :
    finiteCenteredCubeSolutionEnergy a m u k = Book.Ch03.h1EnergyNormOnCube (originCube d k) a (finiteCubeSolutionRestriction a hkm u).toH1

    On an inner scale, the centered energy is the energy of the exact cube restriction.

    source
    noncomputable def HCPolySupport.HighContrast.finiteCenteredCubeBestFitErrorAt {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) (_hkm : k ≤ m) :
    ℝ

    The canonical normalized best-affine error of a finite cube solution on an inner centered cube.

    Equations
    Instances For
      source
      theorem HCPolySupport.HighContrast.finiteCenteredCubeBestFitErrorAt_le {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) (hkm : k ≤ m) (c : ℝ) (e : Vec d) :
      finiteCenteredCubeBestFitErrorAt a m u k hkm ≤ normalizedAffineCandidateError (originCube d k) u.toH1.toFun c e

      The centered-cube best-fit row is no larger than any affine candidate.

      source
      theorem HCPolySupport.HighContrast.finiteCenteredCubeBestFitErrorAt_exists_eq {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) (hkm : k ≤ m) :
      ∃ (c : ℝ) (e : Vec d), finiteCenteredCubeBestFitErrorAt a m u k hkm = normalizedAffineCandidateError (originCube d k) u.toH1.toFun c e

      The centered-cube best-fit row is attained by affine coefficients.

      source
      noncomputable def HCPolySupport.HighContrast.finiteCenteredCubeBestFitInterceptAt {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) :
      ℝ

      The canonical intercept of the affine best fit on an inner centered cube.

      Equations
      Instances For
        source
        noncomputable def HCPolySupport.HighContrast.finiteCenteredCubeBestFitSlopeAt {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) :
        Vec d

        The canonical slope of the affine best fit on an inner centered cube.

        Equations
        Instances For
          source
          theorem HCPolySupport.HighContrast.finiteCenteredCubeBestFitErrorAt_eq_candidate {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (m : ℤ) (u : Book.Ch03.CubeSolution (originCube d m) a) (k : ℤ) (hkm : k ≤ m) :
          finiteCenteredCubeBestFitErrorAt a m u k hkm = normalizedAffineCandidateError (originCube d k) u.toH1.toFun (finiteCenteredCubeBestFitInterceptAt a m u k) (finiteCenteredCubeBestFitSlopeAt a m u k)

          The canonical coefficients attain the centered-cube best-fit error.