FrozenSiteLaw.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Conditioning on a fixed collection of sampled sites

def OAI.JointDickman.frozenSiteMass line 13
Source documentation
Sampled coordinates are fixed; every other coordinate keeps its law.
```
noncomputable def frozenSiteMass (p : ι → A → ℝ) (J : Finset ι) (t : ι → A)
    (i : ι) (a : A) : ℝ :=
…
```
theorem OAI.JointDickman.frozenSiteMass_nonneg line 18
theorem OAI.JointDickman.frozenSiteMass_sum line 25
theorem OAI.JointDickman.frozenSiteMass_average line 30
theorem OAI.JointDickman.frozenSiteMass_support line 45

theorem OAI.JointDickman.frozenSiteMass_disintegrate line 56

Source documentation

Averaging the conditional law recovers the original law. The test may depend on the fixed types, provided only their sampled coordinates matter.

theorem frozenSiteMass_disintegrate (p : ι → A → ℝ)
    (hpone : ∀ i, ∑ a, p i a = 1) (J : Finset ι)
    (F : (ι → A) → (ι → A) → ℝ)
    (hF : ∀ t x, (∀ i ∈ J, x i = t i) → F t x = F x x) :
    finiteExpectation (siteProductMass p) (fun x => F x x) =
      finiteExpectation (siteProductMass p) (fun t =>
        finiteExpectation (siteProductMass (frozenSiteMass p J t)) (F t)) := by
…

Mentions: OAI.JointDickman.finiteExpectation, OAI.JointDickman.frozenSiteMass