Documentation

LeanPool.HighContrastHomogenization.Provider.Response.ProfileEnergyCarriers

High-contrast homogenization: Provider.Response.ProfileEnergyCarriers #

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

Optimizer-energy profile carriers #

The bad branch retains the correlation between the all-scale response maximum and the optimizer energy. The good branch retains only the optimizer energy and the deterministic below-window factor. Both are extended-real L² seminorms, so a divergent maximum remains on the bad branch.

source
noncomputable def HCPolySupport.HighContrast.Response.profileBadEnergy {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (M : CoeffSpace d → ENNReal) (energy : CoeffSpace d → ℝ) :
ENNReal

The correlated bad-event optimizer energy.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.Response.profileGoodEnergy {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (alpha : ℝ) (H : ℕ) (M : CoeffSpace d → ENNReal) (energy : CoeffSpace d → ℝ) :
    ENNReal

    The good-event optimizer energy with its below-window factor.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def HCPolySupport.HighContrast.Response.profileBadEnergyAt {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (lev : ENNReal) (M : CoeffSpace d → ENNReal) (energy : CoeffSpace d → ℝ) :
      ENNReal

      The bad-event optimizer energy at a released split level. The fixed-level carrier is this at lev = 1, definitionally: the event is literally {a | 1 < M a}. The printed threshold factor multiplies the sum of the two branches, so it is carried by the consumer's own outer coefficient and does not appear here.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def HCPolySupport.HighContrast.Response.profileGoodEnergyAt {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (lev : ENNReal) (alpha : ℝ) (H : ℕ) (M : CoeffSpace d → ENNReal) (energy : CoeffSpace d → ℝ) :
        ENNReal

        The good-event optimizer energy at a released split level. The fixed-level carrier is this at lev = 1, definitionally.

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