High-contrast homogenization: Provider.Quenched.CombinedSourceGauge

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

Combining two source scales and their gauges

The maximum of two source scales has a union-bound tail. The factor two is absorbed into a gauge by flooring half of the pointwise minimum at one. Two applications of the original growth inequalities give a growth witness for the combined gauge.

noncomputable def HCPolySupport.HighContrast.Quenched.combinedSourceGauge (Psi₁ Psi₂ : ℝ → ℝ) : ℝ → ℝ

The gauge used for the maximum of two source scales.

Equations

• HCPolySupport.HighContrast.Quenched.combinedSourceGauge Psi₁ Psi₂ t = max 1 (min (Psi₁ t) (Psi₂ t) / 2)

def HCPolySupport.HighContrast.Quenched.combinedSource {Omega : Type u_1} (S₁ S₂ : Omega → ℝ) : Omega → ℝ

The source scale obtained by retaining both source constraints.

Equations

• HCPolySupport.HighContrast.Quenched.combinedSource S₁ S₂ omega = max (S₁ omega) (S₂ omega)

noncomputable def HCPolySupport.HighContrast.Quenched.flooredSourceGauge (Psi : ℝ → ℝ) : ℝ → ℝ

The gauge paired with flooring a source scale at one.

Equations

• HCPolySupport.HighContrast.Quenched.flooredSourceGauge Psi t = if t < 1 then 1 else Psi t

def HCPolySupport.HighContrast.Quenched.flooredSource {Omega : Type u_1} (S : Omega → ℝ) : Omega → ℝ

A source scale floored at one.

Equations

• HCPolySupport.HighContrast.Quenched.flooredSource S omega = max 1 (S omega)

theorem HCPolySupport.HighContrast.Quenched.admissiblePsi_flooredSourceGauge {Psi : ℝ → ℝ} (hPsi : IndependentSums.AdmissiblePsi Psi) : IndependentSums.AdmissiblePsi (flooredSourceGauge Psi)

theorem HCPolySupport.HighContrast.Quenched.hasPsiGrowth_flooredSourceGauge {Psi : ℝ → ℝ} {K : ℝ} (hK : 1 < K) (hPsi : IndependentSums.HasPsiGrowth Psi K) : IndependentSums.HasPsiGrowth (flooredSourceGauge Psi) K

theorem HCPolySupport.HighContrast.Quenched.measurable_flooredSource {Omega : Type u_1} [MeasurableSpace Omega] {S : Omega → ℝ} (hS : Measurable S) : Measurable (flooredSource S)

theorem HCPolySupport.HighContrast.Quenched.one_le_flooredSource {Omega : Type u_1} (S : Omega → ℝ) (omega : Omega) : 1 ≤ flooredSource S omega

theorem HCPolySupport.HighContrast.Quenched.sourceTail_flooredSource {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {Psi : ℝ → ℝ} {S : Omega → ℝ} (htail : ∀ (t : ℝ), 1 ≤ t → P.real (IndependentSums.upperTailEvent S t) ≤ (Psi t)⁻¹) (t : ℝ) : 0 < t → P.real (IndependentSums.upperTailEvent (flooredSource S) t) ≤ (flooredSourceGauge Psi t)⁻¹

theorem HCPolySupport.HighContrast.Quenched.admissiblePsi_combinedSourceGauge {Psi₁ Psi₂ : ℝ → ℝ} (hPsi₁ : IndependentSums.AdmissiblePsi Psi₁) (hPsi₂ : IndependentSums.AdmissiblePsi Psi₂) : IndependentSums.AdmissiblePsi (combinedSourceGauge Psi₁ Psi₂)

theorem HCPolySupport.HighContrast.Quenched.one_le_combinedGrowthWitness (K₁ K₂ : ℝ) : 1 ≤ max 2 (max K₁ K₂) ^ 2

theorem HCPolySupport.HighContrast.Quenched.hasPsiGrowth_combinedSourceGauge {Psi₁ Psi₂ : ℝ → ℝ} {K₁ K₂ : ℝ} (hPsi₁ : IndependentSums.AdmissiblePsi Psi₁) (hPsi₂ : IndependentSums.AdmissiblePsi Psi₂) (hK₁ : 1 < K₁) (hK₂ : 1 < K₂) (hgrowth₁ : IndependentSums.HasPsiGrowth Psi₁ K₁) (hgrowth₂ : IndependentSums.HasPsiGrowth Psi₂ K₂) : IndependentSums.HasPsiGrowth (combinedSourceGauge Psi₁ Psi₂) (max 2 (max K₁ K₂) ^ 2)

theorem HCPolySupport.HighContrast.Quenched.measurable_combinedSource {Omega : Type u_1} [MeasurableSpace Omega] {S₁ S₂ : Omega → ℝ} (hS₁ : Measurable S₁) (hS₂ : Measurable S₂) : Measurable (combinedSource S₁ S₂)

theorem HCPolySupport.HighContrast.Quenched.combinedSource_nonneg {Omega : Type u_1} {S₁ S₂ : Omega → ℝ} (hS₁ : ∀ (omega : Omega), 0 ≤ S₁ omega) (omega : Omega) : 0 ≤ combinedSource S₁ S₂ omega

theorem HCPolySupport.HighContrast.Quenched.sourceTail_combinedSource {Omega : Type u_1} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {Psi₁ Psi₂ : ℝ → ℝ} {S₁ S₂ : Omega → ℝ} (hPsi₁ : IndependentSums.AdmissiblePsi Psi₁) (hPsi₂ : IndependentSums.AdmissiblePsi Psi₂) (htail₁ : ∀ (t : ℝ), 0 < t → P.real (IndependentSums.upperTailEvent S₁ t) ≤ (Psi₁ t)⁻¹) (htail₂ : ∀ (t : ℝ), 0 < t → P.real (IndependentSums.upperTailEvent S₂ t) ≤ (Psi₂ t)⁻¹) (t : ℝ) : 0 < t → P.real (IndependentSums.upperTailEvent (combinedSource S₁ S₂) t) ≤ (combinedSourceGauge Psi₁ Psi₂ t)⁻¹