OAI/Probability/CriticalZ3/ProductCylinder.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ProductCylinder.law line 15
2. instance OAI.ProductCylinder.law_probability line 18
3. def OAI.ProductCylinder.finiteLaw line 21
4. instance OAI.ProductCylinder.finiteLaw_probability line 24
5. theorem OAI.ProductCylinder.map_restrict line 27
6. theorem OAI.ProductCylinder.cylinder_probability line 30
7. theorem OAI.ProductCylinder.cylinder_integral line 35
8. def OAI.ProductCylinder.extend line 42
9. def OAI.ProductCylinder.DeterminedBy line 45
10. theorem OAI.ProductCylinder.determinedBy_eq_extend line 48
11. theorem OAI.ProductCylinder.probability_determined line 54
12. theorem OAI.ProductCylinder.measurableSet_determined line 62
13. theorem OAI.ProductCylinder.map_reindex line 70
14. def OAI.FiniteAssociation.law line 90
15. instance OAI.FiniteAssociation.law_probability line 93
16. def OAI.FiniteAssociation.mean line 96
17. def OAI.FiniteAssociation.extend line 99
18. theorem OAI.FiniteAssociation.extend_mono line 103
19. theorem OAI.FiniteAssociation.extend_false_le_true line 109
20. theorem OAI.FiniteAssociation.mean_mono line 115
21. theorem OAI.FiniteAssociation.mean_option line 119
22. theorem OAI.FiniteAssociation.mean_equiv line 136
23. theorem OAI.FiniteAssociation.increasing line 151

    Source documentation

    Finite product positive association for arbitrary real increasing observables.

    theorem increasing [Fintype E] (p : E → Set.Icc (0 : ℝ) 1)
        (f g : (E → Bool) → ℝ) (hf : Monotone f) (hg : Monotone g) :
        mean p f * mean p g ≤ mean p (fun ω => f ω * g ω) := by
    …

    Mentions: OAI.FiniteAssociation.mean

24. theorem OAI.FiniteAssociation.decreasing line 196

    Source documentation

    Harris association also holds for decreasing observables.

    theorem decreasing [Fintype E] (p : E → Set.Icc (0 : ℝ) 1)
        (f g : (E → Bool) → ℝ) (hf : Antitone f) (hg : Antitone g) :
        mean p f * mean p g ≤ mean p (fun ω => f ω * g ω) := by
    …

    Mentions: OAI.FiniteAssociation.mean

25. def OAI.FiniteAssociation.prob line 202
26. theorem OAI.FiniteAssociation.prob_nonneg line 205
27. theorem OAI.FiniteAssociation.prob_eq_real line 208
28. theorem OAI.FiniteAssociation.indicator_antitone line 213
29. theorem OAI.FiniteAssociation.prob_and line 221
30. theorem OAI.FiniteAssociation.prob_forall line 232

    Source documentation

    The finite-family decreasing-event Harris inequality used for 24 quarter-faces.

    theorem prob_forall [Fintype E] {I : Type uI} (p : E → Set.Icc (0 : ℝ) 1)
        (s : Finset I) (P : I → (E → Bool) → Prop) (hP : ∀ i ∈ s, Antitone (P i)) :
        (∏ i ∈ s, prob p (P i)) ≤ prob p (fun ω => ∀ i ∈ s, P i ω) := by
    …

    Mentions: OAI.FiniteAssociation.prob

31. theorem OAI.ProductCylinder.extend_mono line 252
32. theorem OAI.ProductCylinder.decreasing_forall line 260

    Source documentation

    Harris's finite-family inequality, applied to actual infinite-product cylinder events.

    theorem decreasing_forall {I : Type uI} [Fintype I] (J : Finset E)
        (p : E → Set.Icc (0 : ℝ) 1) (A : I → Set (E → Bool))
        (hA : ∀ i ω ω', (∀ e ∈ J, ω' e = ω e) → (ω' ∈ A i ↔ ω ∈ A i))
        (hmono : ∀ i, Antitone (fun ω => ω ∈ A i)) :
        (∏ i, (law p).real (A i)) ≤ (law p).real (⋂ i, A i) := by
    …

    Mentions: OAI.ProductCylinder.law

33. theorem OAI.ProductCylinder.finite_mass line 287

    Source documentation

    The finite law is a polynomial in its bit parameters.

    theorem finite_mass (J : Finset E) (p : E → Set.Icc (0 : ℝ) 1) (ξ : J → Bool) :
        (finiteLaw J p).real {ξ} = ∏ e : J, if ξ e = true then (p e : ℝ) else 1-(p e : ℝ) := by
    …

    Mentions: OAI.ProductCylinder.finiteLaw

34. theorem OAI.ProductCylinder.continuous_probability line 296