High-contrast homogenization: Provider.Quenched.RenormalizedDaggerCore

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

The renormalized coarse-ellipticity datum

This module combines the native source scale with the random renormalization radius, splits physical cells into the recent window and the older scales, and transports the resulting datum to the triadically rebased law.

noncomputable def HCPolySupport.HighContrast.Quenched.rebasedPullbackSource {d : ℕ} (n : ℕ) (S : CoeffSpace d → ℝ) : CoeffSpace d → ℝ

Pull a source scale on the original samples to the rebased coefficient law.

Equations

• HCPolySupport.HighContrast.Quenched.rebasedPullbackSource n S a = S (HCPolySupport.HighContrast.CoeffSpace.triadicContraction n a)

@[simp]

theorem HCPolySupport.HighContrast.Quenched.rebasedPullbackSource_triadicDilation {d : ℕ} (n : ℕ) (S : CoeffSpace d → ℝ) (a : CoeffSpace d) : rebasedPullbackSource n S (CoeffSpace.triadicDilation n a) = S a

theorem HCPolySupport.HighContrast.Quenched.measurable_rebasedPullbackSource {d : ℕ} (n : ℕ) {S : CoeffSpace d → ℝ} (hS : Measurable S) : Measurable (rebasedPullbackSource n S)

noncomputable def HCPolySupport.HighContrast.Quenched.normalizedNativeSource {d : ℕ} (n : ℕ) (S : CoeffSpace d → ℝ) : CoeffSpace d → ℝ

The native source in the units of the rebased law.

Equations

• HCPolySupport.HighContrast.Quenched.normalizedNativeSource n S = HCPolySupport.HighContrast.Quenched.flooredSource fun (a : HCPolySupport.HighContrast.CoeffSpace d) => S a / 3 ^ n

noncomputable def HCPolySupport.HighContrast.Quenched.normalizedRadiusSource {d : ℕ} (S : CoeffSpace d → ℝ) (Ahat : BlockMat d) (delta rho : ℝ) (h n : ℕ) : CoeffSpace d → ℝ

The renormalization radius in the units of the rebased law.

Equations

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

noncomputable def HCPolySupport.HighContrast.Quenched.renormalizedCombinedSource {d : ℕ} (S : CoeffSpace d → ℝ) (Ahat : BlockMat d) (delta rho : ℝ) (h n : ℕ) : CoeffSpace d → ℝ

The single source scale carrying both the native and renormalized constraints.

Equations

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

noncomputable def HCPolySupport.HighContrast.Quenched.renormalizedCombinedGauge (d n b : ℕ) (mu : ℝ) (Psi : ℝ → ℝ) : ℝ → ℝ

The gauge paired with renormalizedCombinedSource.

Equations

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

noncomputable def HCPolySupport.HighContrast.Quenched.renormalizedCombinedGrowthWitness (d b : ℕ) (mu K : ℝ) : ℝ

The growth witness paired with renormalizedCombinedGauge.

Equations

• HCPolySupport.HighContrast.Quenched.renormalizedCombinedGrowthWitness d b mu K = max 2 (max K (HCPolySupport.HighContrast.Quenched.renormalizedRadiusGrowthWitness d mu b)) ^ 2

theorem HCPolySupport.HighContrast.Quenched.coarseEllipticityDagger_rebased_of_renormalization {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {g rho mu delta Gain : ℝ} {E Ahat : BlockMat d} {Psi : ℝ → ℝ} {K : ℝ} {S : CoeffSpace d → ℝ} {n l0 h b : ℕ} (hdag : CoarseEllipticityDagger P g E Psi K S) (hAhatSymm : IsSymmetricBlockMat Ahat) (hAhat : Book.Ch02.BlockPosDef Ahat) (hdelta : 0 ≤ delta) (hmu : mu = ↑d / 2 - g) (hmupos : 0 < mu) (hgr : g ≤ rho) (hrho : rho ∈ Set.Ico 0 1) (hGain : 0 < Gain) (hl0 : 1 ≤ renormBase g (↑d / 2) mu delta Gain l0 h) (hthr : Real.log 2 ≤ frGaugeConst d * renormBase g (↑d / 2) mu delta Gain l0 h ^ 2 * (3 ^ (2 * mu) - 1)) (hcell : HasCellRenormalization P S Ahat g (↑d / 2) Gain n l0 h) (hb1 : 1 ≤ b) (hh1 : 1 ≤ h) (hbuf : Real.log (2 * renormCellCount d h) ≤ frGaugeConst d * (3 ^ (2 * mu * ↑b) - 1)) (href : BlockMatLoewnerLE E (blockScale (2 * kappaRef E) Ahat)) (hburn : 2 * kappaRef E ≤ (1 + delta) * 3 ^ ((rho - g) * ↑h)) : CoarseEllipticityDagger (triadicRebasedLaw n P) rho (blockScale (1 + delta) Ahat) (renormalizedCombinedGauge d n b mu Psi) (renormalizedCombinedGrowthWitness d b mu K) (rebasedPullbackSource n (renormalizedCombinedSource S Ahat delta rho h n))

The one-time renormalization of the coarse-ellipticity datum, already transported to the rebased coefficient law.