Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.CorrectorDecay.JointNegOneClasses

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.CorrectorDecay.JointNegOneClasses

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

source
theorem HCPolySupport.HighContrast.openCube_h1_grad_memVectorL2 {d : ℕ} {Q : TriadicCube d} (u : H1Function (Book.Ch02.cubeDomain Q).carrier) :
MemVectorL2 (openCubeSet Q) u.grad
source
theorem HCPolySupport.HighContrast.openCube_const_memVectorL2 {d : ℕ} (Q : TriadicCube d) (e : Vec d) :
MemVectorL2 (openCubeSet Q) fun (x : Vec d) => e
source
noncomputable def HCPolySupport.HighContrast.outerFiniteGradientClass {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (e : Vec d) (m : ℤ) :
↥(HilbertVectorL2 (openCubeSet (originCube d m)))

The finite affine gradient defect as an outer-cube quotient class.

Equations
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.outerFiniteFluxClass {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (e : Vec d) (m : ℤ) :
    ↥(HilbertVectorL2 (openCubeSet (originCube d m)))

    The finite affine flux defect as an outer-cube quotient class.

    Equations
    Instances For
      source
      noncomputable def HCPolySupport.HighContrast.innerFiniteGradientClass {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (e : Vec d) (q : ℕ) :
      ↥(HilbertVectorL2 (openCubeSet (originCube d ↑q)))

      The outer finite gradient defect restricted across the fixed gap.

      Equations
      Instances For
        source
        noncomputable def HCPolySupport.HighContrast.innerFiniteFluxClass {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (e : Vec d) (q : ℕ) :
        ↥(HilbertVectorL2 (openCubeSet (originCube d ↑q)))

        The outer finite flux defect restricted across the fixed gap.

        Equations
        Instances For
          source
          noncomputable def HCPolySupport.HighContrast.jointGradientRemainderClass {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (Phi : Vec d → NormalizedLocalH1Carrier d) (e : Vec d) (q : ℕ) :
          ↥(HilbertVectorL2 (openCubeSet (originCube d ↑q)))

          The exact joint gradient minus its fixed-gap finite approximation.

          Equations
          Instances For
            source
            noncomputable def HCPolySupport.HighContrast.jointFluxRemainderClass {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (Phi : Vec d → NormalizedLocalH1Carrier d) (e : Vec d) (q : ℕ) :
            ↥(HilbertVectorL2 (openCubeSet (originCube d ↑q)))

            The exact joint flux defect minus its fixed-gap finite approximation.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem HCPolySupport.HighContrast.correctorGradient_eq_innerFinite_add_remainder {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (Phi : Vec d → NormalizedLocalH1Carrier d) (e : Vec d) (q : ℕ) :
              correctorGradientOnOriginCube Phi e ↑q = innerFiniteGradientClass a e q + jointGradientRemainderClass a Phi e q

              The gradient class is the sum of its restricted finite part and its remainder, as an exact quotient identity.

              source
              theorem HCPolySupport.HighContrast.correctorFlux_eq_innerFinite_add_remainder {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (Phi : Vec d → NormalizedLocalH1Carrier d) (e : Vec d) (q : ℕ) :
              scalarIdentityCorrectorFluxDefectOnOriginCube a Phi e ↑q = innerFiniteFluxClass a e q + jointFluxRemainderClass a Phi e q

              The flux class is the sum of its restricted finite part and its remainder, as an exact quotient identity.

              source
              theorem HCPolySupport.HighContrast.outerFiniteGradient_toVec_ae {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (e : Vec d) (m : ℤ) :
              (fun (x : Vec d) => (↑↑(outerFiniteGradientClass a e m) x).toVec) =ᵐ[volumeMeasureOn (openCubeSet (originCube d m))] fun (x : Vec d) => (finiteAffineSolution a m e).toH1.grad x - e
              source
              theorem HCPolySupport.HighContrast.outerFiniteFlux_toVec_ae {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (e : Vec d) (m : ℤ) :
              (fun (x : Vec d) => (↑↑(outerFiniteFluxClass a e m) x).toVec) =ᵐ[volumeMeasureOn (openCubeSet (originCube d m))] fun (x : Vec d) => matVecMul (Book.Ch03.publicCoeffField (originCube d m) a x) ((finiteAffineSolution a m e).toH1.grad x) - e
              source
              theorem HCPolySupport.HighContrast.jointGradientRemainder_toVec_ae {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (Phi : Vec d → NormalizedLocalH1Carrier d) (hPhi : IsFiniteAffineCorrectionJointLocalEquation a Phi) (e : Vec d) (q : ℕ) :
              (fun (x : Vec d) => (↑↑(jointGradientRemainderClass a Phi e q) x).toVec) =ᵐ[volumeMeasureOn (openCubeSet (originCube d ↑q))] (jointFiniteRemainderCubeSolution a Phi hPhi e q (q + 3) ⋯).toH1.grad

              The quotient remainder has the literal finite-to-joint gradient representative used by the energy telescope.

              source
              theorem HCPolySupport.HighContrast.jointFluxRemainder_toVec_ae {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (Phi : Vec d → NormalizedLocalH1Carrier d) (hPhi : IsFiniteAffineCorrectionJointLocalEquation a Phi) (e : Vec d) (q : ℕ) :
              (fun (x : Vec d) => (↑↑(jointFluxRemainderClass a Phi e q) x).toVec) =ᵐ[volumeMeasureOn (openCubeSet (originCube d ↑q))] fun (x : Vec d) => matVecMul (Book.Ch03.publicCoeffField (originCube d ↑q) a x) ((jointFiniteRemainderCubeSolution a Phi hPhi e q (q + 3) ⋯).toH1.grad x)

              The quotient remainder has the literal finite-to-joint flux representative used by the energy telescope.