FiniteKernels.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Finite dependent sampling kernels

A dependent second draw uses its own normalized mass in each first-draw fiber. In particular, this construction does not replace sequential uniform draws with the generally different uniform law on their sigma type.

structure OAI.LowSpaceSubsetSum.FiniteLaw line 19
def OAI.LowSpaceSubsetSum.FiniteLaw.probability line 28
theorem OAI.LowSpaceSubsetSum.FiniteLaw.probability_nonneg line 32
theorem OAI.LowSpaceSubsetSum.FiniteLaw.probability_true line 40
theorem OAI.LowSpaceSubsetSum.FiniteLaw.probability_mono line 44
theorem OAI.LowSpaceSubsetSum.FiniteLaw.probability_le_one line 56
theorem OAI.LowSpaceSubsetSum.FiniteLaw.probability_compl line 60
def OAI.LowSpaceSubsetSum.FiniteLaw.uniform line 70
theorem OAI.LowSpaceSubsetSum.FiniteLaw.uniform_probability line 77
def OAI.LowSpaceSubsetSum.FiniteLaw.bind line 84
Source documentation
The output retains the preceding draw, making its dependence explicit.
```
noncomputable def bind (μ : FiniteLaw Ω) (Ψ : Ω → Type v)
    [∀ ω, Fintype (Ψ ω)] (K : ∀ ω, FiniteLaw (Ψ ω)) : FiniteLaw (Σ ω, Ψ ω) where
…
```
Mentions: OAI.LowSpaceSubsetSum.FiniteLaw
theorem OAI.LowSpaceSubsetSum.FiniteLaw.bind_probability line 93
theorem OAI.LowSpaceSubsetSum.FiniteLaw.bind_first_probability line 101
theorem OAI.LowSpaceSubsetSum.FiniteLaw.bind_good_lower line 112
theorem OAI.LowSpaceSubsetSum.FiniteLaw.probability_inter_ge_sub line 128
theorem OAI.LowSpaceSubsetSum.FiniteLaw.probability_eq line 140
theorem OAI.LowSpaceSubsetSum.FiniteLaw.bind_point_probability line 147
Source documentation
Conditioning on one retained history leaves exactly its prescribed next-draw law. The formula is valid even when that history has zero mass.
```
theorem bind_point_probability (μ : FiniteLaw Ω) (Ψ : Ω → Type v)
    [∀ ω, Fintype (Ψ ω)] (K : ∀ ω, FiniteLaw (Ψ ω))
    (Q : ∀ ω, Ψ ω → Prop) (ω : Ω) :
    (μ.bind Ψ K).probability (fun z => z.1 = ω ∧ Q z.1 z.2) =
      μ.mass ω * (K ω).probability (Q ω) := by
…
```
Mentions: OAI.LowSpaceSubsetSum.FiniteLaw, OAI.LowSpaceSubsetSum.FiniteLaw.probability
theorem OAI.LowSpaceSubsetSum.FiniteLaw.bind_conditional_probability line 160