High-contrast homogenization: Annealed.Witness

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

The hypothesis set of the random-source theorems is satisfiable

t.polynomial.entry quantifies over laws that are stationary under integer translations, have unit range of dependence, and satisfy the coarse ellipticity condition e.coarse.ellipticity. Nothing in those statements exhibits a law that satisfies all three, so on their own they leave open the possibility that the hypothesis set is empty and the conclusion vacuous. This file closes that possibility with an explicit law.

The witness is the Dirac law at the constant identity coefficient field, with source scale identically zero, gauge Ψ(t) = e^t, growth witness K = 2, reference block (4d+1) times the doubled identity, and discount exponent g = 0. Stationarity holds because the constant field is fixed by integer translation; independence holds because under an atomic law every pair of events is independent; the source tail is trivial because the upper tail events of the zero source at positive levels are empty; and the coarse domination is the scale-uniform bound of the constant field, which needs no discount factor.

The Dirac law also carries the measurability of the coarse response, which e.Theta.m presupposes for Θ_m.

The gauge

theorem HCPolySupport.HighContrast.admissiblePsi_exp : IndependentSums.AdmissiblePsi Real.exp

The exponential is an admissible gauge: increasing on ℝ_+ with values in [1, ∞).

theorem HCPolySupport.HighContrast.hasPsiGrowth_exp : IndependentSums.HasPsiGrowth Real.exp 2

The exponential gauge has growth witness 2: t e^t ≤ e^{2t} for t ≥ 1.

The witness law

noncomputable def HCPolySupport.HighContrast.witnessLaw (d : ℕ) : MeasureTheory.Measure (CoeffSpace d)

The witness law: the Dirac law at the constant identity coefficient field.

Equations

• HCPolySupport.HighContrast.witnessLaw d = MeasureTheory.Measure.dirac (HCPolySupport.HighContrast.constIdentity d)

instance HCPolySupport.HighContrast.instIsProbabilityMeasureWitnessLaw {d : ℕ} : MeasureTheory.IsProbabilityMeasure (witnessLaw d)

theorem HCPolySupport.HighContrast.isStationaryLaw_witnessLaw {d : ℕ} : IsStationaryLaw (witnessLaw d)

The witness law is stationary: the constant identity field is fixed by every integer translation.

theorem HCPolySupport.HighContrast.isUnitRangeLaw_dirac {d : ℕ} (a : CoeffSpace d) : IsUnitRangeLaw (MeasureTheory.Measure.dirac a)

Every atomic law has unit range of dependence: under a Dirac law the indicator of an intersection is the product of the indicators, so any two sigma-fields coarser than the global one are independent.

theorem HCPolySupport.HighContrast.isUnitRangeLaw_witnessLaw {d : ℕ} : IsUnitRangeLaw (witnessLaw d)

The source scale

theorem HCPolySupport.HighContrast.upperTailEvent_zero {d : ℕ} {t : ℝ} (ht : 0 < t) : IndependentSums.upperTailEvent (fun (x : CoeffSpace d) => 0) t = ∅

At a positive level the upper tail event of the zero source is empty.

The coarse ellipticity assumption

theorem HCPolySupport.HighContrast.blockScale_discount_zero {d : ℕ} (E : BlockMat d) (m k : ℤ) : blockScale (3 ^ (0 * (↑m - ↑k))) E = E

At the exponent g = 0 the discount factor 3^{g(m-k)} is one.

theorem HCPolySupport.HighContrast.one_le_discount {g : ℝ} (hg : 0 ≤ g) {m k : ℤ} (hkm : k ≤ m) : 1 ≤ 3 ^ (g * (↑m - ↑k))

At a nonnegative exponent the discount factor 3^{g(m-k)} is at least one on the scales k ≤ m of e.coarse.ellipticity.

theorem HCPolySupport.HighContrast.coarseEllipticityDagger_witnessLaw_of_mem_Ico {d : ℕ} {g : ℝ} (hg : g ∈ Set.Ico 0 1) : CoarseEllipticityDagger (witnessLaw d) g (witnessRefBlock d) Real.exp 2 fun (x : CoeffSpace d) => 0

The witness law satisfies e.coarse.ellipticity at every admissible discount exponent, with the doubled-identity reference block, the exponential gauge, growth witness 2, and the zero source scale.

theorem HCPolySupport.HighContrast.coarseEllipticityDagger_witnessLaw {d : ℕ} : CoarseEllipticityDagger (witnessLaw d) 0 (witnessRefBlock d) Real.exp 2 fun (x : CoeffSpace d) => 0

The witness law at the exponent g = 0, at which the discount factor is one.

The coarse response is measurable under an atomic law

theorem HCPolySupport.HighContrast.hasMeasurableCoarseBlock_dirac {d : ℕ} (a : CoeffSpace d) (U : Set (Vec d)) : HasMeasurableCoarseBlock (MeasureTheory.Measure.dirac a) U

Under an atomic law every entry of the coarse response is almost surely strongly measurable: the well-formedness that e.Theta.m presupposes.

theorem HCPolySupport.HighContrast.hasMeasurableCoarseBlock_witnessLaw {d : ℕ} (U : Set (Vec d)) : HasMeasurableCoarseBlock (witnessLaw d) U

The hypothesis set is satisfiable

theorem HCPolySupport.HighContrast.exists_law_satisfying_hypotheses (d : ℕ) : ∃ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P ∧ IsStationaryLaw P ∧ IsUnitRangeLaw P ∧ CoarseEllipticityDagger P 0 E Ψ K S

The law-side hypothesis set of t.polynomial.entry is satisfiable, in every dimension and with no further restriction: the Dirac law at the constant identity field, with the doubled-identity reference block, the exponential gauge, growth witness 2, and the zero source scale, satisfies all four hypotheses at the discount exponent g = 0.

theorem HCPolySupport.HighContrast.exists_law_satisfying_hypotheses_of_mem_Ico (d : ℕ) {g : ℝ} (hg : g ∈ Set.Ico 0 1) : ∃ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P ∧ IsStationaryLaw P ∧ IsUnitRangeLaw P ∧ CoarseEllipticityDagger P g E Ψ K S

The hypothesis set is satisfiable at every admissible discount exponent, so no branch of the quantifier over g in t.polynomial.entry is vacuous.