High-contrast homogenization: Provider.Quenched.SmallContrastMeanSlotConversionAt

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

The mean slot's conversion at a supplied comparability

The mean-to-reference conversion takes a variance normalized at the adapted mean into one normalized at the reference block, and it builds its own comparability from the entry estimate, so its constant is cF · kap2Value. Everything in that argument past the comparability step is generic: the only fact used about the constant is that the reference is dominated by that multiple of the mean.

This file isolates that generic half. scaleVariance_mean_le_of_comparability takes the domination as a hypothesis, and entry_scaleVariance_mean_le_reference_at reads it from a comparability constant supplied by the caller. At the isotropy carriers the caller already holds such a constant — the same one the row cap uses — and it is a function of the near-identity defect alone, so the conversion factor meanSlotConversionAt names no geometric carrier.

noncomputable def HCPolySupport.HighContrast.Quenched.meanSlotConversionAt (d : ℕ) (cF kap : ℝ) : ℝ

The mean-slot conversion at a supplied comparability constant. The kap2Value of the entry route is replaced by the caller's own constant.

Equations

• HCPolySupport.HighContrast.Quenched.meanSlotConversionAt d cF kap = √(2 * ↑d) * (cF * kap)

theorem HCPolySupport.HighContrast.Quenched.meanSlotConversionAt_nonneg (d : ℕ) {cF kap : ℝ} (hcF0 : 0 ≤ cF) (hkap0 : 0 ≤ kap) : 0 ≤ meanSlotConversionAt d cF kap

theorem HCPolySupport.HighContrast.Quenched.scaleVariance_mean_le_of_comparability {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} {t : ℤ} (hEt : Book.Ch02.BlockPosDef (adaptedMean P q t)) {F : BlockMat d} (hFsym : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {cP : ℝ} (hcP0 : 0 ≤ cP) (hF2le : BlockMatLoewnerLE F (blockScale cP (adaptedMean P q t))) (hXm : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => schattenSize 2 (blockSub (coarseBlock (adaptedCell q t) a) (adaptedMean P q t)) (adaptedMean P q t)) P) : scaleVariance P q (adaptedMean P q t) t ≤ ENNReal.ofReal (√(2 * ↑d) * cP) * scaleVariance P q F t

The generic half of the conversion. Once the reference is dominated by a multiple of the adapted mean, the normalized variance transfers with that multiple and a dimensional Schatten factor.

theorem HCPolySupport.HighContrast.Quenched.entry_scaleVariance_mean_le_reference_at {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} {E : BlockMat d} {t : ℤ} (hEt : Book.Ch02.BlockPosDef (adaptedMean P q t)) {F : BlockMat d} (hFsym : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {cF kap : ℝ} (hcF0 : 0 ≤ cF) (hkap0 : 0 ≤ kap) (hFeq : F = blockScale cF E) (hcomp : ∀ (X : BlockVec d), blockVecDot X (blockMatVecMul E X) ≤ kap * blockVecDot X (blockMatVecMul (adaptedMean P q t) X)) (hXm : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => schattenSize 2 (blockSub (coarseBlock (adaptedCell q t) a) (adaptedMean P q t)) (adaptedMean P q t)) P) : scaleVariance P q (adaptedMean P q t) t ≤ ENNReal.ofReal (meanSlotConversionAt d cF kap) * scaleVariance P q F t

The conversion at a supplied comparability constant. The caller's constant replaces the entry route's kap2Value, and with it every geometric carrier leaves the conversion factor.

theorem HCPolySupport.HighContrast.Quenched.entry_supply_mean_slot_bound_at {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} {E : BlockMat d} {t : ℤ} (hEt : Book.Ch02.BlockPosDef (adaptedMean P q t)) {F : BlockMat d} (hFsym : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {cF kap : ℝ} (hcF0 : 0 ≤ cF) (hkap0 : 0 ≤ kap) (hFeq : F = blockScale cF E) (hcomp : ∀ (X : BlockVec d), blockVecDot X (blockMatVecMul E X) ≤ kap * blockVecDot X (blockMatVecMul (adaptedMean P q t) X)) {V0 : ℝ} (hterm : scaleVariance P q F t ≤ ENNReal.ofReal V0) (hXm : MeasureTheory.AEStronglyMeasurable (fun (a : CoeffSpace d) => schattenSize 2 (blockSub (coarseBlock (adaptedCell q t) a) (adaptedMean P q t)) (adaptedMean P q t)) P) : scaleVariance P q (adaptedMean P q t) t ≤ ENNReal.ofReal (meanSlotConversionAt d cF kap * V0)

The mean slot at a supplied comparability constant.