Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.Corrector.PushforwardFamilyCore

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.Corrector.PushforwardFamilyCore

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

The pushforward corrector family: definitions and the corrector equation #

The identity-gauge producer reduces the stationary corrector family clause to RootNormalizedSupply, a change of comparison matrix: it asks the certificate for an identity-gauge weak-error row, while the root's certificate supplies an abar-gauge one. No lemma anywhere transports between the two.

This module executes the architectural repair. The physical corrector is defined as the affine pushforward of the normalized-gauge one, so the certificate-side demand becomes the normalized-gauge datum the converter already produces.

This module carries the normalized-gauge event and its invariant core, the pushforward value and gradient families, and the two clauses that need no gauge algebra: the weak-gradient pair on Set.univ and the physical corrector equation. The slope-linearity and integer-covariance clauses, the marker and the hole itself are in PushforwardGaugeAlgebra and PushforwardFamilyClauses.

The normalized-gauge event and its invariant core #

source
def HCPolySupport.HighContrast.Root.pushforwardEventSet (d : ℕ) [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) :
Set (CoeffSpace d)

The samples whose normalized-gauge reading carries the intrinsic datum.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def HCPolySupport.HighContrast.Root.pushforwardCore (d : ℕ) [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) :
    Set (CoeffSpace d)

    Its invariant core under integer translations of the physical sample.

    Equations
    Instances For
      source
      theorem HCPolySupport.HighContrast.Root.pushforwardEvent_of_mem_core {d : ℕ} [NeZero d] {abar : Mat d} {hS : Matrix.PosDef (symmPart abar)} {a : CoeffSpace d} (ha : a ∈ pushforwardCore d abar hS) (z : Fin d → ℤ) :
      RootCorrectorEvent d (normalizedSample abar hS (translateCoeff z a))
      source
      theorem HCPolySupport.HighContrast.Root.pushforwardEvent_of_mem_core_self {d : ℕ} [NeZero d] {abar : Mat d} {hS : Matrix.PosDef (symmPart abar)} {a : CoeffSpace d} (ha : a ∈ pushforwardCore d abar hS) :
      RootCorrectorEvent d (normalizedSample abar hS a)

      Transporting almost-everywhere identities through the gauge #

      source
      theorem HCPolySupport.HighContrast.Root.quasiMeasurePreserving_matVecMul_gaugeRootInv {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) :
      MeasureTheory.QuasiMeasurePreserving (matVecMul (gaugeRoot abar)⁻¹) MeasureTheory.volume MeasureTheory.volume

      The inverse gauge root is quasi-measure-preserving on Vec d.

      The pushforward family #

      source
      noncomputable def HCPolySupport.HighContrast.Root.pushforwardPhysicalPhi (d : ℕ) [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) :
      Vec d → CoeffSpace d → Vec d → ℝ

      The pushforward value family: the affine pushforward of the normalized-gauge carrier at the pulled-back slope, extended by zero off the invariant core.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def HCPolySupport.HighContrast.Root.pushforwardPhysicalGradPhi (d : ℕ) [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) :
        Vec d → CoeffSpace d → Vec d → Vec d

        The pushforward gradient family.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem HCPolySupport.HighContrast.Root.pushforwardPhysicalPhi_of_mem {d : ℕ} [NeZero d] {abar : Mat d} {hS : Matrix.PosDef (symmPart abar)} {a : CoeffSpace d} (ha : a ∈ pushforwardCore d abar hS) (e : Vec d) :
          pushforwardPhysicalPhi d abar hS e a = pushforwardValue abar (rootJointCarrier d (matVecMul (gaugeRoot abar) e) (normalizedSample abar hS a))
          source
          theorem HCPolySupport.HighContrast.Root.pushforwardPhysicalGradPhi_of_mem {d : ℕ} [NeZero d] {abar : Mat d} {hS : Matrix.PosDef (symmPart abar)} {a : CoeffSpace d} (ha : a ∈ pushforwardCore d abar hS) (e : Vec d) :
          pushforwardPhysicalGradPhi d abar hS e a = pushforwardGradient abar (rootJointCarrier d (matVecMul (gaugeRoot abar) e) (normalizedSample abar hS a))

          The corrector equation #

          source
          theorem HCPolySupport.HighContrast.Root.memLiouvilleClass_gaugeCoeff_rootJointCarrier {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (a : CoeffSpace d) (e : Vec d) (hevent : RootCorrectorEvent d (normalizedSample abar hS a)) :
          MemLiouvilleClass (gaugeCoeff a abar hS) rootCorrectorGrowth (fun (y : Vec d) => vecDot (matVecMul (gaugeRoot abar) e) y + (rootJointCarrier d (matVecMul (gaugeRoot abar) e) (normalizedSample abar hS a)).globalValueRepresentative y) fun (y : Vec d) => matVecMul (gaugeRoot abar) e + (rootJointCarrier d (matVecMul (gaugeRoot abar) e) (normalizedSample abar hS a)).globalGradientRepresentative y

          The normalized-gauge Liouville membership of the selected carrier at a pulled-back slope, from the datum's value-growth row.

          source
          theorem HCPolySupport.HighContrast.Root.pushforwardPhysical_equation (d : ℕ) [NeZero d] (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) {a : CoeffSpace d} (ha : a ∈ pushforwardCore d abar hS) (e : Vec d) :
          HasWeakGradientOn Set.univ (pushforwardPhysicalPhi d abar hS e a) (pushforwardPhysicalGradPhi d abar hS e a) ∧ IsWeakSolutionOn (fun (y : Vec d) => ↑↑a y) Set.univ fun (y : Vec d) => e + pushforwardPhysicalGradPhi d abar hS e a y

          On the core the pushforward pair is a global weak-gradient pair and solves the physical corrector equation at every slope.