Documentation

LeanPool.HighContrastHomogenization.Provider.Response.ProfileWeakCarriers

High-contrast homogenization: Provider.Response.ProfileWeakCarriers #

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

Annealed centers and weak profile quantities #

The primal and adjoint centers are formed independently by averaging the two slots of their terminal optimizer states. The weak quantities use the concrete scale-average seminorm, and the centering variances use the diagonal metric quadratic form. A coefficient transformation is kept explicit so the same carriers apply to a fixed skew recentering without changing the ambient probability space.

source
noncomputable def HCPolySupport.HighContrast.Response.profilePrimalCenter {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) :
BlockVec d

The separately annealed primal optimizer center.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.Response.profileAdjointCenter {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) :
    BlockVec d

    The separately annealed coefficient-transpose optimizer center.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def HCPolySupport.HighContrast.Response.profilePrimalWeakRoot {d : ℕ} (m0 : Mat d) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) (center : BlockVec d) (a : CoeffSpace d) :
      ENNReal

      The normalized primal weak seminorm of one coefficient sample.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def HCPolySupport.HighContrast.Response.profileAdjointWeakRoot {d : ℕ} (m0 : Mat d) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) (center : BlockVec d) (a : CoeffSpace d) :
        ENNReal

        The normalized adjoint weak seminorm of one coefficient sample.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def HCPolySupport.HighContrast.Response.profilePrimalWeakQuantity {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (m0 : Mat d) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) :
          ENNReal

          The primal weak quantity is the square of the normalized L² seminorm.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem HCPolySupport.HighContrast.Response.profilePrimalWeakQuantity_eq {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (m0 : Mat d) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) :
            profilePrimalWeakQuantity P m0 hq t sample p r = MeasureTheory.eLpNorm (profilePrimalWeakRoot m0 hq t sample p r (profilePrimalCenter P hq t sample p r)) 2 P ^ 2

            The defining equation of the primal weak quantity.

            source
            noncomputable def HCPolySupport.HighContrast.Response.profileAdjointWeakQuantity {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (m0 : Mat d) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) :
            ENNReal

            The adjoint weak quantity is the square of its normalized L² seminorm.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem HCPolySupport.HighContrast.Response.profileAdjointWeakQuantity_eq {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (m0 : Mat d) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) :
              profileAdjointWeakQuantity P m0 hq t sample p r = MeasureTheory.eLpNorm (profileAdjointWeakRoot m0 hq t sample p r (profileAdjointCenter P hq t sample p r)) 2 P ^ 2

              The defining equation of the adjoint weak quantity.

              source
              noncomputable def HCPolySupport.HighContrast.Response.profilePrimalCenterVariance {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (m0 : Mat d) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) :
              ENNReal

              The primal centering variance in the canonical diagonal metric.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                noncomputable def HCPolySupport.HighContrast.Response.profileAdjointCenterVariance {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (m0 : Mat d) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (sample : CoeffSpace d → CoeffSpace d) (p r : Vec d) :
                ENNReal

                The adjoint centering variance in the canonical diagonal metric.

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