FactorSampling.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.UniqueGamesTheorem.Inverse.FactorSampling.fullAverage line 15
def OAI.UniqueGamesTheorem.Inverse.FactorSampling.nonzeroFlow line 18
def OAI.UniqueGamesTheorem.Inverse.FactorSampling.zeroMass line 21
theorem OAI.UniqueGamesTheorem.Inverse.FactorSampling.boundary_indicator line 25
theorem OAI.UniqueGamesTheorem.Inverse.FactorSampling.boundary_mass line 32
Source documentation
The overlap of the two zero-factor events is subtracted exactly once.
```
theorem boundary_mass (p : A → ℝ) (q : B → ℝ)
    (hp : IsProbability p) (hq : IsProbability q) :
    fullAverage p q (fun a b => if a = 0 ∨ b = 0 then 1 else 0) = zeroMass p q := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.FactorSampling.fullAverage, OAI.UniqueGamesTheorem.Inverse.FactorSampling.zeroMass
theorem OAI.UniqueGamesTheorem.Inverse.FactorSampling.fullAverage_eq_zeroMass_add_nonzeroFlow line 54
Source documentation
A self-loop occurs whenever either perturbation factor is zero.
```
theorem fullAverage_eq_zeroMass_add_nonzeroFlow (p : A → ℝ) (q : B → ℝ)
    (hp : IsProbability p) (hq : IsProbability q) (h : A → B → ℝ)
    (hleft : ∀ b, h 0 b = 1) (hright : ∀ a, h a 0 = 1) :
    fullAverage p q h = zeroMass p q + nonzeroFlow p q h := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.FactorSampling.fullAverage, OAI.UniqueGamesTheorem.Inverse.FactorSampling.zeroMass, OAI.UniqueGamesTheorem.Inverse.FactorSampling.nonzeroFlow
def OAI.UniqueGamesTheorem.Inverse.FactorSampling.conditionedRetention line 81
theorem OAI.UniqueGamesTheorem.Inverse.FactorSampling.fullAverage_eq_mixture line 84
theorem OAI.UniqueGamesTheorem.Inverse.FactorSampling.conditionedRetention_ge_half line 97
Source documentation
This is the full sampling-law implication, rather than only the scalar inequality under an assumed mixture identity.
```
theorem conditionedRetention_ge_half (p : A → ℝ) (q : B → ℝ)
    (hp : IsProbability p) (hq : IsProbability q) (h : A → B → ℝ)
    (hleft : ∀ b, h 0 b = 1) (hright : ∀ a, h a 0 = 1)
    {η : ℝ} (hη : 0 < η) (hη1 : η < 1)
    (hzero : 0 ≤ zeroMass p q) (hzeroη : zeroMass p q ≤ η / 2)
    (haccept : η ≤ fullAverage p q h) : η / 2 ≤ conditionedRetention p q h := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.FactorSampling.zeroMass, OAI.UniqueGamesTheorem.Inverse.FactorSampling.fullAverage, OAI.UniqueGamesTheorem.Inverse.FactorSampling.conditionedRetention
theorem OAI.UniqueGamesTheorem.Inverse.FactorSampling.zeroMass_binary_uniform line 111
Source documentation
Specialization of the excluded zero-factor mass to uniform binary vector spaces. The powers are supplied by the cardinalities, so the formula also keeps track of the overlap when both factors are zero.
```
theorem zeroMass_binary_uniform (p : A → ℝ) (q : B → ℝ) (ell m : ℕ)
    (hp0 : p 0 = ((2 : ℝ) ^ ell)⁻¹) (hq0 : q 0 = ((2 : ℝ) ^ m)⁻¹) :
    zeroMass p q = ((2 : ℝ) ^ ell)⁻¹ + ((2 : ℝ) ^ m)⁻¹ - ((2 : ℝ) ^ (ell + m))⁻¹ := by
…
```
Mentions: OAI.UniqueGamesTheorem.Inverse.FactorSampling.zeroMass