High-contrast homogenization: Entry.Source.Multiplier

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

The source stopping minimum

Near e.source.multiplier, l.source.whitney. The finite source-center success events, stationary union and Markov bounds, and measurable least successful offset. The multiplier is returned as a characterized existential witness: there is no new definition. Failure at every depth receives representative offset zero; the source moment estimate proves that exceptional event null.

theorem HCPolySupport.HighContrast.Source.measurableSet_source_success {d : ℕ} (S : CoeffSpace d → ℝ) (hS : Measurable S) (jStar r : ℕ) : MeasurableSet {a : CoeffSpace d | ∀ (w : Fin d → ℤ), standardCellCenter (↑(jStar + r)) w ∈ centeredCube d ↑(2 * jStar + r) → S (translateCoeff (fun (i : Fin d) => 3 ^ (jStar + r) * w i) a) ≤ 3 ^ (jStar + r)}

The success events in the printed minimum are measurable.

theorem HCPolySupport.HighContrast.Source.source_failure_probability_le {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (S : CoeffSpace d → ℝ) (hS : Measurable S) (hS0 : ∀ (a : CoeffSpace d), 0 ≤ S a) (hstat : IsStationaryLaw P) (p : ℝ) (hp : 0 < p) (hi : MeasureTheory.Integrable (fun (a : CoeffSpace d) => S a ^ p) P) (jStar r : ℕ) : P.real {a : CoeffSpace d | ¬∀ (w : Fin d → ℤ), standardCellCenter (↑(jStar + r)) w ∈ centeredCube d ↑(2 * jStar + r) → S (translateCoeff (fun (i : Fin d) => 3 ^ (jStar + r) * w i) a) ≤ 3 ^ (jStar + r)} ≤ (3 ^ (d * jStar) * ∫ (a : CoeffSpace d), S a ^ p ∂P) / (3 ^ (jStar + r)) ^ p

Stationarity and Markov's inequality bound failure at one depth. Independence is unused.

theorem HCPolySupport.HighContrast.Source.ae_exists_source_success {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (S : CoeffSpace d → ℝ) (hS : Measurable S) (hS0 : ∀ (a : CoeffSpace d), 0 ≤ S a) (hstat : IsStationaryLaw P) (p : ℝ) (hp : 0 < p) (hi : MeasureTheory.Integrable (fun (a : CoeffSpace d) => S a ^ p) P) (jStar : ℕ) : ∀ᵐ (a : CoeffSpace d) ∂P, ∃ (r : ℕ), ∀ (w : Fin d → ℤ), standardCellCenter (↑(jStar + r)) w ∈ centeredCube d ↑(2 * jStar + r) → S (translateCoeff (fun (i : Fin d) => 3 ^ (jStar + r) * w i) a) ≤ 3 ^ (jStar + r)

Finite source moments make the all-failure event null, without a lower-scale burn.

theorem HCPolySupport.HighContrast.Source.measurable_least_offset {Ω : Type u_1} [MeasurableSpace Ω] (Good : ℕ → Ω → Prop) (hm : ∀ (r : ℕ), MeasurableSet {a : Ω | Good r a}) : ∃ (ell : Ω → ℕ), Measurable ell ∧ (∀ (a : Ω), (∃ (r : ℕ), Good r a) → Good (ell a) a ∧ ∀ (r : ℕ), Good r a → ell a ≤ r) ∧ (∀ (a : Ω), (¬∃ (r : ℕ), Good r a) → ell a = 0) ∧ ∀ (a : Ω), ∀ r < ell a, ¬Good r a

A measurable least successful offset, with value zero if every attempt fails. The events need not be monotone. This is a measurable representative on the original sigma algebra, so no completion of the probability space is required.

theorem HCPolySupport.HighContrast.Source.source_minimum {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (γ : ℝ) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) (hstat : IsStationaryLaw P) (hdag : CoarseEllipticityDagger P γ E Ψ K S) (jStar : ℕ) : have Good := fun (r : ℕ) (a : CoeffSpace d) => ∀ (w : Fin d → ℤ), standardCellCenter (↑(jStar + r)) w ∈ centeredCube d ↑(2 * jStar + r) → S (translateCoeff (fun (i : Fin d) => 3 ^ (jStar + r) * w i) a) ≤ 3 ^ (jStar + r); ∃ (ell : CoeffSpace d → ℕ) (X : CoeffSpace d → ℝ), Measurable ell ∧ Measurable X ∧ (∀ (a : CoeffSpace d), X a = 3 ^ (γ * ↑(ell a))) ∧ (∀ (a : CoeffSpace d), (¬∃ (r : ℕ), Good r a) → ell a = 0) ∧ (∀ᵐ (a : CoeffSpace d) ∂P, Good (ell a) a ∧ (∀ (r : ℕ), Good r a → ell a ≤ r) ∧ ∀ (r : ℕ), Good r a → X a ≤ 3 ^ (γ * ↑r)) ∧ (γ = 0 → ∀ (a : CoeffSpace d), X a = 1) ∧ ∀ (p : ℝ), 1 ≤ p → ∀ (r : ℕ), P.real {a : CoeffSpace d | r < ell a} ≤ (3 ^ (d * jStar) * ∫ (a : CoeffSpace d), S a ^ p ∂P) / (3 ^ (jStar + r)) ^ p

The printed source minimum is attained almost surely. The representative is one on the all-failure null set, and is identically one when the exponent is zero. No rounding or source lower-scale threshold is needed for attainment alone.

theorem HCPolySupport.HighContrast.Source.stopping_lintegral_le {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (ell : Ω → ℕ) (hell : Measurable ell) (b A q : ℝ) (hb : 0 ≤ b) (hA : 0 ≤ A) (hq : 0 ≤ q) (hbq : b * q < 1) (htail : ∀ (r : ℕ), μ.real {a : Ω | r < ell a} ≤ A * q ^ r) : ∫⁻ (a : Ω), ENNReal.ofReal (b ^ ell a) ∂μ ≤ ENNReal.ofReal (1 + b * A / (1 - b * q))

Summing the upper tail of a natural offset gives a finite exponential moment. This is an extended-integral estimate; integrability is a consequence, not a premise.

theorem HCPolySupport.HighContrast.Source.source_threshold_constant (C B δ : ℝ) (hC : 0 < C) (hB : 0 < B) (hδ : 0 < δ) : have Csrc := (C + max 1 (Real.logb 2 B)) / δ; 0 < Csrc ∧ ∀ (K : ℝ), 1 < K → ∀ (jStar : ℕ), ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → B * K ^ C ≤ 3 ^ (δ * ↑jStar)

An explicit constant for the closed source lower-scale threshold. The formula is fixed before the growth witness and scale, and introduces no additive burn.

theorem HCPolySupport.HighContrast.Source.source_tail_power_identity (d jStar r : ℕ) (p M : ℝ) : 3 ^ (d * jStar) * M / (3 ^ (jStar + r)) ^ p = M / 3 ^ ((p - ↑d) * ↑jStar) * (3 ^ (-p)) ^ r

Separate the fixed source-window factor from the geometric offset tail.

theorem HCPolySupport.HighContrast.Source.memLp_and_norm_le_two_of_lintegral {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (X : Ω → ℝ) (hX : Measurable X) (hX0 : ∀ (a : Ω), 0 ≤ X a) (Q : ℕ) (hQ : 0 < Q) (hbound : ∫⁻ (a : Ω), ENNReal.ofReal (X a ^ Q) ∂μ ≤ ENNReal.ofReal (2 ^ Q)) : MeasureTheory.MemLp X (ENNReal.ofReal ↑Q) μ ∧ MeasureTheory.Integrable (fun (a : Ω) => X a ^ Q) μ ∧ ∫ (a : Ω), X a ^ Q ∂μ ≤ 2 ^ Q ∧ MeasureTheory.eLpNorm X (ENNReal.ofReal ↑Q) μ ≤ ENNReal.ofReal 2

A finite nonnegative moment supplies membership before its actual norm is bounded.

theorem HCPolySupport.HighContrast.Source.source_multiplier (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) [MeasureTheory.IsProbabilityMeasure P] (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), IsStationaryLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → have Good := fun (r : ℕ) (a : CoeffSpace d) => ∀ (w : Fin d → ℤ), standardCellCenter (↑(jStar + r)) w ∈ centeredCube d ↑(2 * jStar + r) → S (translateCoeff (fun (i : Fin d) => 3 ^ (jStar + r) * w i) a) ≤ 3 ^ (jStar + r); ∃ (ell : CoeffSpace d → ℕ) (X : CoeffSpace d → ℝ), Measurable ell ∧ Measurable X ∧ (∀ (a : CoeffSpace d), X a = 3 ^ (γ * ↑(ell a))) ∧ (∀ᵐ (a : CoeffSpace d) ∂P, Good (ell a) a ∧ (∀ (r : ℕ), Good r a → ell a ≤ r) ∧ ∀ (r : ℕ), Good r a → X a ≤ 3 ^ (γ * ↑r)) ∧ MeasureTheory.MemLp X (ENNReal.ofReal ↑(bigQ d γ)) P ∧ MeasureTheory.Integrable (fun (a : CoeffSpace d) => X a ^ bigQ d γ) P ∧ ∫ (a : CoeffSpace d), X a ^ bigQ d γ ∂P ≤ 2 ^ bigQ d γ ∧ MeasureTheory.eLpNorm X (ENNReal.ofReal ↑(bigQ d γ)) P ≤ ENNReal.ofReal 2

The printed, characterized source multiplier and its fixed selection-moment bound. Write p=2*(d+Q), b=3^(γ*Q), q=3^(-p), and let C be the source-moment constant supplied by source_selection_moment_bound. We choose, once before the law, B=C*b/(1-b*q) and Csrc=(C+max 1 (logb 2 B))/(p-d). The standing threshold is closed, with no extra burn.