Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.UnitRangeMeanBlock

High-contrast homogenization: Provider.Quenched.UnitRangeMeanBlock #

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

The mean block of a block-valued observable #

The concentration estimate centres each observable at its own mean, so the renormalization argument needs to compare the block of those means with the annealed block. The printed argument makes that comparison one-sided and free of error terms: the truncated block is below the coarse block at every sample, because the cutoff multiplies a positive block by a factor at most one, and the mean is monotone.

This file records the block of entrywise means, identifies its quadratic form as the average of the quadratic forms, and proves the monotonicity that the printed argument uses. The annealed block is the mean block of the coarse block, so the comparison specializes to it.

The mean block #

source
noncomputable def HCPolySupport.HighContrast.Quenched.meanBlock {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (M : CoeffSpace d → BlockMat d) :
BlockMat d

The block of entrywise means of a block-valued observable.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.HighContrast.Quenched.annealedBlock_eq_meanBlock {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (U : Set (Vec d)) :
    annealedBlock P U = meanBlock P fun (a : CoeffSpace d) => coarseBlock U a

    The annealed block is the mean block of the coarse block.

    source
    theorem HCPolySupport.HighContrast.Quenched.blockMatEntry_meanBlock {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (M : CoeffSpace d → BlockMat d) (α β : BlockCoord d) :
    blockMatEntry (meanBlock P M) α β = ∫ (a : CoeffSpace d), blockMatEntry (M a) α β ∂P

    The entries of the mean block are the integrals of the entries.

    source
    def HCPolySupport.HighContrast.Quenched.HasIntegrableBlock {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (M : CoeffSpace d → BlockMat d) :
    Prop

    The entrywise integrability of a block-valued observable.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.HighContrast.Quenched.hasIntegrableBlock_coarseBlock {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {U : Set (Vec d)} (hint : HasIntegrableCoarseBlock P U) :
      HasIntegrableBlock P fun (a : CoeffSpace d) => coarseBlock U a
      source
      theorem HCPolySupport.HighContrast.Quenched.integrable_blockVecDot_of_hasIntegrableBlock {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {M : CoeffSpace d → BlockMat d} (hint : HasIntegrableBlock P M) (X : BlockVec d) :
      MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockVecDot X (blockMatVecMul (M a) X)) P

      The quadratic form of a block-valued observable is integrable as soon as its entries are.

      source
      theorem HCPolySupport.HighContrast.Quenched.blockVecDot_meanBlock_eq_integral {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {M : CoeffSpace d → BlockMat d} (hint : HasIntegrableBlock P M) (X : BlockVec d) :
      blockVecDot X (blockMatVecMul (meanBlock P M) X) = ∫ (a : CoeffSpace d), blockVecDot X (blockMatVecMul (M a) X) ∂P

      The quadratic form of the mean block is the average of the quadratic forms.

      Monotonicity of the mean #

      source
      theorem HCPolySupport.HighContrast.Quenched.blockMatLoewnerLE_meanBlock {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {M N : CoeffSpace d → BlockMat d} (hM : HasIntegrableBlock P M) (hN : HasIntegrableBlock P N) (hle : ∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (M a) (N a)) :
      BlockMatLoewnerLE (meanBlock P M) (meanBlock P N)

      The mean block is monotone. A block-valued observable dominated at almost every sample has a dominated mean. This is the printed step 𝐀hom(□_l) ≥ E[Ã_z], one-sided and free of error terms.