High-contrast homogenization: Provider.Quenched.CoupledMixingScale

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

A coupled mixing-scale certificate

The mixing scale, its marginal tail, and its pathwise all-later certificate belong to one witness. Keeping these data together prevents replacing the selected scale by an unrelated random variable with the same marginal tail.

structure HCPolySupport.HighContrast.Quenched.CoupledMixingScaleWitness {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) (selectedRow : ℕ → Ω → ℝ) (cMix cd eta kappa delta : ℝ) : Type u_1

One selected mixing scale together with the row series and bad events from which it was constructed.

• stoppingNormalization : ℝ

  Normalization multiplying the random scale in the eventual exclusion of bad events.

• normalization : ℝ

  Final normalization, at least three times the stopping normalization.

• scale : Ω → ℝ

  Measurable random scale with the prescribed stretched-exponential tail bound.

• row : ℕ → Ω → ℝ

  Selected nonnegative row sequence whose weighted tails determine the bad events.

• tailSum : ℕ → Ω → ℝ

  Sum of the row tail weighted by 3 ^ (kappa * j) from each starting generation.

• bad : ℕ → Set Ω

  Bad event where the weighted row tail is at least delta.

• one_le_stoppingNormalization : 1 ≤ self.stoppingNormalization
• one_le_normalization : 1 ≤ self.normalization
• three_mul_stoppingNormalization_le : 3 * self.stoppingNormalization ≤ self.normalization
• measurable_scale : Measurable self.scale
• one_le_scale (ω : Ω) : 1 ≤ self.scale ω
• scale_tail (t : ℝ) : 1 ≤ t → P.real {ω : Ω | cMix * t ≤ self.scale ω} ≤ Real.exp (-cd * t ^ eta)
• row_eq_selected (n : ℕ) (ω : Ω) : self.row n ω = selectedRow n ω
• row_nonneg (n : ℕ) (ω : Ω) : 0 ≤ self.row n ω
• hasSum_tail : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), HasSum (fun (j : ℕ) => 3 ^ (kappa * ↑j) * self.row (n + j) ω) (self.tailSum n ω)
• bad_eq (n : ℕ) : self.bad n = {ω : Ω | delta ≤ self.tailSum n ω}
• measurableSet_bad (n : ℕ) : MeasurableSet (self.bad n)
• eventually_not_mem_bad : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), self.stoppingNormalization * self.scale ω ≤ 3 ^ n → ω ∉ self.bad n

theorem HCPolySupport.HighContrast.Quenched.CoupledMixingScaleWitness.mem_bad_iff {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {selectedRow : ℕ → Ω → ℝ} {cMix cd eta kappa delta : ℝ} (W : CoupledMixingScaleWitness P selectedRow cMix cd eta kappa delta) (n : ℕ) (ω : Ω) : ω ∈ W.bad n ↔ delta ≤ W.tailSum n ω

Membership in a selected bad event is the literal tail-sum threshold.

theorem HCPolySupport.HighContrast.Quenched.CoupledMixingScaleWitness.tailSum_lt_of_not_mem_bad {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {selectedRow : ℕ → Ω → ℝ} {cMix cd eta kappa delta : ℝ} (W : CoupledMixingScaleWitness P selectedRow cMix cd eta kappa delta) {n : ℕ} {ω : Ω} (hgood : ω ∉ W.bad n) : W.tailSum n ω < delta

Absence of a bad event makes the corresponding weighted tail sum strictly smaller than its threshold.

theorem HCPolySupport.HighContrast.Quenched.CoupledMixingScaleWitness.weighted_row_le_tailSum {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {selectedRow : ℕ → Ω → ℝ} {cMix cd eta kappa delta : ℝ} (W : CoupledMixingScaleWitness P selectedRow cMix cd eta kappa delta) (n j : ℕ) (ω : Ω) (hsum : HasSum (fun (i : ℕ) => 3 ^ (kappa * ↑i) * W.row (n + i) ω) (W.tailSum n ω)) : 3 ^ (kappa * ↑j) * W.row (n + j) ω ≤ W.tailSum n ω

Every nonnegative summand is bounded by the selected tail sum.

theorem HCPolySupport.HighContrast.Quenched.CoupledMixingScaleWitness.weighted_row_lt_of_not_mem_bad {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {selectedRow : ℕ → Ω → ℝ} {cMix cd eta kappa delta : ℝ} (W : CoupledMixingScaleWitness P selectedRow cMix cd eta kappa delta) {n j : ℕ} {ω : Ω} (hsum : HasSum (fun (i : ℕ) => 3 ^ (kappa * ↑i) * W.row (n + i) ω) (W.tailSum n ω)) (hgood : ω ∉ W.bad n) : 3 ^ (kappa * ↑j) * W.row (n + j) ω < delta

One later row is strictly controlled by the corresponding weighted-series threshold whenever the starting event is good.

theorem HCPolySupport.HighContrast.Quenched.CoupledMixingScaleWitness.eventually_weighted_row_lt {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {selectedRow : ℕ → Ω → ℝ} {cMix cd eta kappa delta : ℝ} (W : CoupledMixingScaleWitness P selectedRow cMix cd eta kappa delta) : ∀ᵐ (ω : Ω) ∂P, ∀ (n j : ℕ), W.stoppingNormalization * W.scale ω ≤ 3 ^ n → 3 ^ (kappa * ↑j) * W.row (n + j) ω < delta

On one common full-measure event, the same selected mixing scale controls every later weighted row.