Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.EnergyPrice.WindowedFrozenWitnessPrice

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.EnergyPrice.WindowedFrozenWitnessPrice

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

The frozen-witness price with an arbitrary law-free coarse-graining window #

An earlier form carried 𝓔 ≀ 1 as a binder. The upstream ellipticity control inv_mul_LambdaSq_finite_two_le_card_mul_homogenizationError_sq_add_one holds for any value of 𝓔, so a law-free bound 𝓔 ≀ Cwit suffices and only replaces the window 4d by 2d(CwitΒ² + 1).

This file re-threads the whole chain with that window as a parameter: ellipticity β†’ cube energy norm β†’ cube price β†’ translated-cube price β†’ frozen-witness price. Setting Cwit = 1 recovers the unit-energy constants.

The windowed coarse ellipticity #

source
def HCPolySupport.HighContrast.EnergyPrice.ellipticityWindow (d : β„•) (Cwit : ℝ) :
ℝ

The coarse-graining window produced by a weak-error bound Cwit.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.EnergyPrice.ellipticityWindow_nonneg (d : β„•) (Cwit : ℝ) :
    0 ≀ ellipticityWindow d Cwit
    source
    theorem HCPolySupport.HighContrast.EnergyPrice.lambdaSq_finite_two_le_of_identityError_le {d : β„•} [NeZero d] (Q : TriadicCube d) (a : Book.Ch02.TriadicCoeffFamily d) {s Cwit : ℝ} (hs : 0 < s) (_hCwit : 0 ≀ Cwit) (herr : Book.Ch02.HomogenizationErrorOnCube Q s Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) a 1 ≀ Cwit) :
    Book.Ch02.LambdaSq Q s (Book.Ch02.MultiscaleExponent.finite 2) a ≀ ellipticityWindow d Cwit

    The windowed ellipticity bound.

    source
    theorem HCPolySupport.HighContrast.EnergyPrice.poincareUpperEllipticityFactor_le_of_identityError_le {d : β„•} [NeZero d] (Q : TriadicCube d) (a : Book.Ch03.CoeffFamily d) {s Cwit : ℝ} (hs : 0 < s) (hCwit : 0 ≀ Cwit) (herr : Book.Ch02.HomogenizationErrorOnCube Q s Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) a 1 ≀ Cwit) :
    Book.Ch03.poincareUpperEllipticityFactor Q a s (Book.Ch02.MultiscaleExponent.finite 2) ≀ (ellipticityWindow d Cwit).rpow (1 / 2)

    The windowed upper coarse ellipticity factor.

    The windowed constants #

    source
    noncomputable def HCPolySupport.HighContrast.EnergyPrice.lawFreeCubeEnergyConstantW (C : ℝ) (d : β„•) (s Cwit : ℝ) :
    ℝ

    The windowed law-free cube constant.

    Equations
    Instances For
      source
      theorem HCPolySupport.HighContrast.EnergyPrice.lawFreeCubeEnergyConstantW_nonneg (C : ℝ) (d : β„•) (s Cwit : ℝ) :
      0 ≀ lawFreeCubeEnergyConstantW C d s Cwit
      source
      noncomputable def HCPolySupport.HighContrast.EnergyPrice.gaugeCubeEnergyPriceW (C : ℝ) (d : β„•) (s Cwit ell : ℝ) :
      ℝ

      The windowed cube price.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def HCPolySupport.HighContrast.EnergyPrice.gaugeWitnessEnergyPriceW (C : ℝ) (d : β„•) (s Cwit : ℝ) (abar : Mat d) :
        ℝ

        The windowed frozen-witness price. Klawfree(d,s,Cwit) times the eccentricity power d + 2s.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The windowed chain #

          source
          theorem HCPolySupport.HighContrast.EnergyPrice.exists_windowedDirichletCubeEnergyNormBound (d : β„•) [NeZero d] :
          βˆƒ (C : ℝ), 0 < C ∧ βˆ€ (Q : TriadicCube d) (a : Book.Ch03.CoeffFamily d) (s Cwit : ℝ) (v : Book.Ch03.DirichletForcedCubeSolution Q a 0), 0 < s β†’ s < 1 β†’ 0 ≀ Cwit β†’ Book.Ch03.ForceBesovRegularity Q s (Book.Ch03.dirichletBoundaryGradientField v) β†’ Book.Ch02.HomogenizationErrorOnCube Q s Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) a 1 ≀ Cwit β†’ Book.Ch03.dirichletForcedSolutionEnergyNorm Q a v ≀ C * s.rpow (-(1 / 2)) * (ellipticityWindow d Cwit).rpow (1 / 2) * Book.Ch03.scaleNormalizedPositiveBesovVectorNormTwo Q s (Book.Ch03.dirichletBoundaryGradientField v)

          The windowed un-squared cube energy bound.

          source
          theorem HCPolySupport.HighContrast.EnergyPrice.exists_windowedPriceAtTranslatedCubeWitness (d : β„•) [NeZero d] :
          βˆƒ (C : ℝ), 0 < C ∧ βˆ€ (Q : TriadicCube d) (z : Vec d) (a : Book.Ch03.CoeffFamily d) (s Cwit : ℝ) (v : Book.Ch03.DirichletForcedCubeSolution Q a 0) (bTrans : CoeffField d) (uGrad FTrans : Vec d β†’ Vec d), 0 < s β†’ s < 1 β†’ 0 ≀ Cwit β†’ Book.Ch03.ForceBesovRegularity Q s (Book.Ch03.dirichletBoundaryGradientField v) β†’ MemVectorL2 (openCubeSet Q) (Book.Ch03.dirichletBoundaryGradientField v) β†’ Book.Ch02.HomogenizationErrorOnCube Q s Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) a 1 ≀ Cwit β†’ (βˆ€ (y : Vec d), bTrans (y + z) = (a.coeffOn Q).toCoeffField y) β†’ (βˆ€ (y : Vec d), uGrad (y + z) = v.toH1.grad y) β†’ (βˆ€ (y : Vec d), FTrans (y + z) = Book.Ch03.dirichletBoundaryGradientField v y) β†’ 0 ≀ gaugeCubeEnergyPriceW C d s Cwit (cubeScaleFactor Q) ∧ (eVolumeAverage (translateSet z (openCubeSet Q)) fun (x : Vec d) => ENNReal.ofReal (coefficientEnergyDensity bTrans uGrad x)) ≀ ENNReal.ofReal (gaugeCubeEnergyPriceW C d s Cwit (cubeScaleFactor Q)) * hsNormSq (translateSet z (openCubeSet Q)) s FTrans

          The windowed price on a translate of a triadic cube.

          source
          theorem HCPolySupport.HighContrast.EnergyPrice.exists_windowedGaugePhysicalEnergyPriceAtFrozenWitness (d : β„•) [NeZero d] :
          βˆƒ (C : ℝ), 0 < C ∧ βˆ€ (abar : Mat d), Matrix.PosDef (symmPart abar) β†’ βˆ€ (U : Set (Vec d)) (j : β„€) (z : Vec d) (s Cwit : ℝ) (aFam : Book.Ch03.CoeffFamily d) (v : Book.Ch03.DirichletForcedCubeSolution (originCube d j) aFam 0) (aHat : CoeffField d) (uHat : H1Function (matImage (matSqrt (symmPart abar))⁻¹ U)) (g0grad FTrans : Vec d β†’ Vec d), 0 < s β†’ s < 1 / 2 β†’ 0 ≀ Cwit β†’ U = (fun (x : Vec d) => z + matVecMul (matSqrt (symmPart abar)) x) '' openCubeSet (originCube d j) β†’ U βŠ† ellipsoid abar 1 β†’ ellipsoid abar (1 / (3 * βˆšβ†‘d)) βŠ† U β†’ Book.Ch03.ForceBesovRegularity (originCube d j) s (Book.Ch03.dirichletBoundaryGradientField v) β†’ MemVectorL2 (openCubeSet (originCube d j)) (Book.Ch03.dirichletBoundaryGradientField v) β†’ Book.Ch02.HomogenizationErrorOnCube (originCube d j) s Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) aFam 1 ≀ Cwit β†’ (βˆ€ (y : Vec d), aHat (y + matVecMul (matSqrt (symmPart abar))⁻¹ z) = (aFam.coeffOn (originCube d j)).toCoeffField y) β†’ (βˆ€ (y : Vec d), uHat.grad (y + matVecMul (matSqrt (symmPart abar))⁻¹ z) = v.toH1.grad y) β†’ (βˆ€ (y : Vec d), FTrans (y + matVecMul (matSqrt (symmPart abar))⁻¹ z) = Book.Ch03.dirichletBoundaryGradientField v y) β†’ (βˆ€ (x : Vec d), FTrans (matVecMul (matSqrt (symmPart abar))⁻¹ x) = matVecMul (matSqrt (symmPart abar)) (g0grad x)) β†’ RowSupply.GaugePhysicalEnergyPriceAtWitness (matImage (matSqrt (symmPart abar))⁻¹ U) aHat uHat (gaugeWitnessEnergyPriceW C d s Cwit abar) (hsNormSq U s fun (x : Vec d) => matVecMul (matSqrt (symmPart abar)) (g0grad x))

          The windowed capstone price at the frozen witness.