ResamplingDensity.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LeanBlast.SecondKahnKalai.resamplingExperimentLaw line 16
theorem OAI.LeanBlast.SecondKahnKalai.resamplingExperiment_expectation line 27
theorem OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation_resampling_source line 41
Source documentation
Mixture expansion before using the Bernoulli union identity.
```
theorem bernoulliExpectation_resampling_source (ν : FiniteLaw B) (A : B → Finset X)
    (ρ : ℝ) (F : Finset X → ℝ) :
    bernoulliExpectation ρ (fun W => ν.expectation (fun c => F (resamplingY A W c))) =
      ∑ c, ν.weight c * bernoulliExpectation ρ (fun W => F (W ∪ A c)) := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation, OAI.LeanBlast.SecondKahnKalai.resamplingY
theorem OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation_resamplingZ line 55
Source documentation
Expand the proposed density into the finite mixture of conditional Bernoulli densities. This is an algebraic identity, not a normalization premise.
```
theorem bernoulliExpectation_resamplingZ (ν : FiniteLaw B) (A : B → Finset X)
    (ρ : ℝ) (F : Finset X → ℝ) :
    bernoulliExpectation ρ (fun Y => resamplingZ ν A ρ Y * F Y) =
      ∑ c, ν.weight c * bernoulliExpectation ρ
        (fun Y => if A c ⊆ Y then F Y / ρ ^ (A c).card else 0) := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation, OAI.LeanBlast.SecondKahnKalai.resamplingZ
theorem OAI.LeanBlast.SecondKahnKalai.resampling_source_density line 72
theorem OAI.LeanBlast.SecondKahnKalai.resampling_density line 81
theorem OAI.LeanBlast.SecondKahnKalai.resampling_density_prob line 98
Source documentation
Event form of the observed-set density formula, used for small-Z failure events in the actual resampling procedure.
```
theorem resampling_density_prob (ν : FiniteLaw B) (A : B → Finset X)
    {ρ : ℝ} (hν : ν.IsPositive) (hρ : 0 < ρ) (P : Finset X → Prop) :
    bernoulliExpectation ρ (fun W => (resamplingLaw ν A ρ W hν hρ).prob
      (fun cb => P (resamplingY A W cb.1))) =
      bernoulliExpectation ρ (fun Y => if P Y then resamplingZ ν A ρ Y else 0) := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.bernoulliExpectation, OAI.LeanBlast.SecondKahnKalai.resamplingLaw, OAI.LeanBlast.SecondKahnKalai.resamplingY, OAI.LeanBlast.SecondKahnKalai.resamplingZ
theorem OAI.LeanBlast.SecondKahnKalai.resamplingExperiment_density line 107
theorem OAI.LeanBlast.SecondKahnKalai.resamplingExperiment_density_prob line 116
theorem OAI.LeanBlast.SecondKahnKalai.resamplingExperiment_observed_mass line 128
Source documentation
Every atom of the observed-set law is exactly the Bernoulli atom times the explicit finite density Z.
```
theorem resamplingExperiment_observed_mass (ν : FiniteLaw B) (A : B → Finset X)
    {ρ : ℝ} (hν : ν.IsPositive) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (Y : Finset X) :
    (resamplingExperimentLaw ν A ρ hν hρ hρ1).prob
      (fun ω => resamplingY A ω.1 ω.2.1 = Y) =
      bernoulliWeight ρ Y * resamplingZ ν A ρ Y := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.resamplingExperimentLaw, OAI.LeanBlast.SecondKahnKalai.resamplingY, OAI.LeanBlast.SecondKahnKalai.bernoulliWeight, OAI.LeanBlast.SecondKahnKalai.resamplingZ