High-contrast homogenization: Provider.Quenched.CoupledPhysicalBlockDecay

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

Physical block decay from a coupled mixing scale

The common replay scale uses the selected mixing scale and restored source from the same sample. The quotient-dilation identity then turns decay of the hatted row at generation m into decay of the original coefficient at generation N + m.

def HCPolySupport.HighContrast.Quenched.coupledNormalizedScale {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {selectedRow : ℕ → CoeffSpace d → ℝ} {cMix cd eta kappa delta : ℝ} (W : CoupledMixingScaleWitness P selectedRow cMix cd eta kappa delta) (Ssrc : CoeffSpace d → ℝ) (a : CoeffSpace d) : ℝ

The common normalized scale before restoring the annealed dilation.

Equations

• HCPolySupport.HighContrast.Quenched.coupledNormalizedScale W Ssrc a = W.normalization * max 1 (max (W.scale a) (Ssrc a))

def HCPolySupport.HighContrast.Quenched.coupledPhysicalLength {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {selectedRow : ℕ → CoeffSpace d → ℝ} {cMix cd eta kappa delta : ℝ} (N : ℕ) (W : CoupledMixingScaleWitness P selectedRow cMix cd eta kappa delta) : ℝ

The physical replay length obtained by undoing N triadic dilations.

Equations

• HCPolySupport.HighContrast.Quenched.coupledPhysicalLength N W = 3 ^ N * W.normalization

def HCPolySupport.HighContrast.Quenched.coupledPhysicalScale {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {selectedRow : ℕ → CoeffSpace d → ℝ} {cMix cd eta kappa delta : ℝ} (N : ℕ) (W : CoupledMixingScaleWitness P selectedRow cMix cd eta kappa delta) (Ssrc : CoeffSpace d → ℝ) (a : CoeffSpace d) : ℝ

The physical random scale obtained by undoing N triadic dilations.

Equations

• HCPolySupport.HighContrast.Quenched.coupledPhysicalScale N W Ssrc a = 3 ^ N * HCPolySupport.HighContrast.Quenched.coupledNormalizedScale W Ssrc a

def HCPolySupport.HighContrast.Quenched.HasAllLaterPhysicalBlockRowFromAnnealedScale {d : ℕ} (rho kappa C : ℝ) (Abar : BlockMat d) (S : CoeffSpace d → ℝ) (N : ℕ) (X : CoeffSpace d → ℝ) (a : CoeffSpace d) : Prop

Every natural generation above the restored annealed scale has the source-restricted block-row decay.

Equations

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

noncomputable def HCPolySupport.HighContrast.Quenched.physicalBlockRowAtInteger {d : ℕ} (rho : ℝ) (Abar : BlockMat d) (S : CoeffSpace d → ℝ) (a : CoeffSpace d) (m : ℤ) : ℝ

The physical block row at an integer generation. Negative generations are represented by generation zero; when the random scale is at least one, the defining scale premise makes that branch impossible.

Equations

• HCPolySupport.HighContrast.Quenched.physicalBlockRowAtInteger rho Abar S a m = HCPolySupport.HighContrast.Quenched.quenchedBlockRow rho Abar (S a) a m.toNat

def HCPolySupport.HighContrast.Quenched.HasAllLaterPhysicalBlockRow {d : ℕ} (rho kappa C : ℝ) (Abar : BlockMat d) (S X : CoeffSpace d → ℝ) (a : CoeffSpace d) : Prop

Block-row decay at every admissible integer physical generation.

Equations

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

theorem HCPolySupport.HighContrast.Quenched.CoupledMixingScaleWitness.eventually_hasAllLaterPhysicalBlockRowFromAnnealedScale {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {cMix cd eta kappa delta rho C : ℝ} {Abar : BlockMat d} {S : CoeffSpace d → ℝ} {N : ℕ} (W : CoupledMixingScaleWitness P (fun (m : ℕ) (a : CoeffSpace d) => quenchedBlockRow rho Abar (max 1 (S a / 3 ^ N)) (physicalScaleCoefficient N a) m) cMix cd eta kappa delta) (hkappa : 0 < kappa) (hdelta : 0 < delta) (hdeltaC : delta ≤ C) : ∀ᵐ (a : CoeffSpace d) ∂P, HasAllLaterPhysicalBlockRowFromAnnealedScale rho kappa C Abar S N (coupledPhysicalScale N W fun (a : CoeffSpace d) => max 1 (S a / 3 ^ N)) a

The a.e. same-witness certificate gives physical all-later block decay. No decay implication is assumed as part of the coupled witness.

theorem HCPolySupport.HighContrast.Quenched.CoupledMixingScaleWitness.eventually_hasAllLaterPhysicalBlockRow {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {cMix cd eta kappa delta rho C : ℝ} {Abar : BlockMat d} {S : CoeffSpace d → ℝ} {N : ℕ} (W : CoupledMixingScaleWitness P (fun (m : ℕ) (a : CoeffSpace d) => quenchedBlockRow rho Abar (max 1 (S a / 3 ^ N)) (physicalScaleCoefficient N a) m) cMix cd eta kappa delta) (hkappa : 0 < kappa) (hdelta : 0 < delta) (hdeltaC : delta ≤ C) : ∀ᵐ (a : CoeffSpace d) ∂P, HasAllLaterPhysicalBlockRow rho kappa C Abar S (coupledPhysicalScale N W fun (a : CoeffSpace d) => max 1 (S a / 3 ^ N)) a

The natural offset estimate extends to every integer physical generation: the scale lower bound first forces that generation to lie above N.