High-contrast homogenization: Provider.Quenched.TriadicRebasedSource

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

Source and gauge under triadic rebasing

The rebased source is measured in units of the enlarged microscopic scale. Its tail is therefore governed by the original gauge evaluated at the correspondingly dilated argument.

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

The source scale of a rebased coefficient sample, expressed in the new microscopic units.

Equations

• HCPolySupport.HighContrast.triadicRebasedSource n S a = S (HCPolySupport.HighContrast.CoeffSpace.triadicContraction n a) / 3 ^ n

def HCPolySupport.HighContrast.triadicRebasedGauge (n : ℕ) (Ψ : ℝ → ℝ) : ℝ → ℝ

The gauge naturally paired with triadicRebasedSource.

Equations

• HCPolySupport.HighContrast.triadicRebasedGauge n Ψ t = Ψ (3 ^ n * t)

@[simp]

theorem HCPolySupport.HighContrast.triadicRebasedSource_triadicDilation {d : ℕ} (n : ℕ) (S : CoeffSpace d → ℝ) (a : CoeffSpace d) : triadicRebasedSource n S (CoeffSpace.triadicDilation n a) = S a / 3 ^ n

Evaluating the rebased source on a dilated sample recovers the original source divided by the scale factor.

theorem HCPolySupport.HighContrast.measurable_triadicRebasedSource {d : ℕ} (n : ℕ) {S : CoeffSpace d → ℝ} (hS : Measurable S) : Measurable (triadicRebasedSource n S)

Measurability of the source is preserved by rebasing.

theorem HCPolySupport.HighContrast.triadicRebasedSource_nonneg {d : ℕ} (n : ℕ) {S : CoeffSpace d → ℝ} (hS : ∀ (a : CoeffSpace d), 0 ≤ S a) (a : CoeffSpace d) : 0 ≤ triadicRebasedSource n S a

Nonnegativity of the source is preserved by rebasing.

theorem HCPolySupport.HighContrast.admissiblePsi_triadicRebasedGauge (n : ℕ) {Ψ : ℝ → ℝ} (hΨ : IndependentSums.AdmissiblePsi Ψ) : IndependentSums.AdmissiblePsi (triadicRebasedGauge n Ψ)

Admissibility of the gauge is preserved by positive dilation of its argument.

theorem HCPolySupport.HighContrast.hasPsiGrowth_triadicRebasedGauge (n : ℕ) {Ψ : ℝ → ℝ} {K : ℝ} (hΨ : IndependentSums.AdmissiblePsi Ψ) (hgrowth : IndependentSums.HasPsiGrowth Ψ K) : IndependentSums.HasPsiGrowth (triadicRebasedGauge n Ψ) K

The same growth witness works for the rebased gauge.

theorem HCPolySupport.HighContrast.sourceTail_triadicRebasedLaw {d : ℕ} (n : ℕ) {P : MeasureTheory.Measure (CoeffSpace d)} {Ψ : ℝ → ℝ} {S : CoeffSpace d → ℝ} (hSmeas : Measurable S) (htail : ∀ (t : ℝ), 0 < t → P.real (IndependentSums.upperTailEvent S t) ≤ (Ψ t)⁻¹) (t : ℝ) : 0 < t → (triadicRebasedLaw n P).real (IndependentSums.upperTailEvent (triadicRebasedSource n S) t) ≤ (triadicRebasedGauge n Ψ t)⁻¹

The source tail transports exactly through the mapped coefficient law.