FiniteConditioning.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Finite Conditioning

def OAI.HadwigerCounterexample.nbr line 16
Source documentation
Number of solutions as a real.
```
def nbr (p : A → Prop) := tot (fun x => ind (p x))
```
Mentions: OAI.HadwigerCounterexample.tot, OAI.HadwigerCounterexample.ind
def OAI.HadwigerCounterexample.onW line 18
theorem OAI.HadwigerCounterexample.nbr_eq_card line 20
theorem OAI.HadwigerCounterexample.pr_unif line 26
theorem OAI.HadwigerCounterexample.unifOn_val line 32
theorem OAI.HadwigerCounterexample.unifOn_sub line 35
theorem OAI.HadwigerCounterexample.unifOn_carried line 38
theorem OAI.HadwigerCounterexample.on_unif line 41
theorem OAI.HadwigerCounterexample.unifOn_true line 49
theorem OAI.HadwigerCounterexample.pr_on line 52
theorem OAI.HadwigerCounterexample.pr_of_on line 59
theorem OAI.HadwigerCounterexample.onW_val line 69
theorem OAI.HadwigerCounterexample.on_mon line 72
theorem OAI.HadwigerCounterexample.uniform_support line 80
Source documentation
Being a probability with support p and all point masses there equal uniquely characterizes unifOn.
```
theorem uniform_support {w : Wgt A} {p : A → Prop} (hw : IsLaw w)
    (hp : carried w p) (he : ∀ x y, p x → p y → w x = w y) :
    w = unifOn p := by
…
```
Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.IsLaw, OAI.HadwigerCounterexample.carried, OAI.HadwigerCounterexample.unifOn
theorem OAI.HadwigerCounterexample.avg_bij line 97
theorem OAI.HadwigerCounterexample.mapW_carried line 105

theorem OAI.HadwigerCounterexample.uniform_orbit line 115

Source documentation

Pointwise transitivity transfer of a uniform law under observation.

theorem uniform_orbit {p : A → Prop} {q : B → Prop} (f : A → B) (hp : ∃ x, p x)
    (hq : ∀ x, p x → q (f x))
    (h : ∀ y z, q y → q z → ∃ e : A ≃ A, (∀ x, p x ↔ p (e x))
      ∧ ∀ x, f x = y ↔ f (e x)=z) :
    mapW (unifOn p) f = unifOn q := by
…

Mentions: OAI.HadwigerCounterexample.mapW, OAI.HadwigerCounterexample.unifOn

theorem OAI.HadwigerCounterexample.disintegrate line 129
Source documentation
A pointwise fiber disintegration.
```
theorem disintegrate {w : Wgt A} (hw : ∀ x, 0 ≤ w x) (f : A → B) :
    w = mixW (mapW w f) (fun y => onW w (fun x => f x = y)) := by
…
```
Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.mixW, OAI.HadwigerCounterexample.mapW, OAI.HadwigerCounterexample.onW
theorem OAI.HadwigerCounterexample.mapW_cap line 145
Source documentation
Mapping changes a density bound functorially.
```
theorem mapW_cap {w v : Wgt A} {c : ℝ} (h : ∀ x, w x ≤ c * v x) (f : A → B) (y) :
    mapW w f y ≤ c * mapW v f y := by
…
```
Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.mapW