OAI/Probability/CriticalZ3/Conditioning.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InfiniteConditioning.replace line 17
2. def OAI.InfiniteConditioning.fixedParameter line 20
3. def OAI.InfiniteConditioning.pattern line 24
4. theorem OAI.InfiniteConditioning.measurable_replace line 28
5. theorem OAI.InfiniteConditioning.measurableSet_pattern line 35
6. theorem OAI.InfiniteConditioning.replace_eq_of_pattern line 41
7. theorem OAI.InfiniteConditioning.map_replace line 49
8. abbrev OAI.InfiniteConditioning.bitSigma line 65
9. theorem OAI.InfiniteConditioning.measurable_replace_compl line 69
10. theorem OAI.InfiniteConditioning.measurable_pattern_sigma line 79
11. theorem OAI.InfiniteConditioning.pattern_inter line 90

    Source documentation

    Literal finite-history factorization, including impossible histories.

    theorem pattern_inter (p : E → Set.Icc (0 : ℝ) 1) (J : Finset E) (ξ : E → Bool)
        (A : Set (E → Bool)) (hA : MeasurableSet A) :
        ProductCylinder.law p (pattern J ξ ∩ A) =
          ProductCylinder.law p (pattern J ξ) * ProductCylinder.law (fixedParameter p J ξ) A := by
    …

    Mentions: OAI.ProductCylinder.law, OAI.InfiniteConditioning.pattern, OAI.InfiniteConditioning.fixedParameter

12. theorem OAI.InfiniteConditioning.pattern_inter_real line 112
13. theorem OAI.InfiniteConditioning.pattern_extend_iff line 120
14. theorem OAI.InfiniteConditioning.measure_select line 130

    Source documentation

    Partition a finite reveal without conditioning on any unrevealed event.

    theorem measure_select (p : E → Set.Icc (0 : ℝ) 1) (J : Finset E)
        (A : (J → Bool) → Set (E → Bool)) (hA : ∀ a, MeasurableSet (A a)) :
        (ProductCylinder.law p).real {ω | ω ∈ A (J.restrict ω)} =
          ∑ a : J → Bool, (ProductCylinder.law p).real (pattern J (ProductCylinder.extend J a)) *
            (ProductCylinder.law (fixedParameter p J (ProductCylinder.extend J a))).real (A a) := by
    …

    Mentions: OAI.ProductCylinder.law, OAI.InfiniteConditioning.pattern, OAI.ProductCylinder.extend, OAI.InfiniteConditioning.fixedParameter

15. theorem OAI.InfiniteConditioning.sum_pattern_real line 149
16. theorem OAI.InfiniteConditioning.fixedParameter_congr line 155
17. theorem OAI.InfiniteConditioning.measurableSet_select line 163
18. theorem OAI.InfiniteConditioning.measurable_determined_sigma line 180
19. theorem OAI.InfiniteConditioning.indepSet_determined line 200

    Source documentation

    Arbitrary observables of disjoint finite blocks are independent under the infinite product law, also when other coordinates have been fixed to 0 or 1.

    theorem indepSet_determined (p : E → Set.Icc (0 : ℝ) 1) (J K : Finset E)
        (hJK : Disjoint J K) (A B : Set (E → Bool))
        (hA : ProductCylinder.DeterminedBy (F := Prop) J (fun ω => ω ∈ A))
    …

    Mentions: OAI.ProductCylinder.DeterminedBy

20. theorem OAI.InfiniteConditioning.disjoint_blocks_probability line 214
21. def OAI.InfiniteConditioning.bitProbability line 253
22. theorem OAI.InfiniteConditioning.single_probability line 256
23. theorem OAI.InfiniteConditioning.finite_pattern_probability line 269
24. def OAI.InfiniteConditioning.allValue line 284
25. theorem OAI.InfiniteConditioning.allValue_determined line 286
26. theorem OAI.InfiniteConditioning.measurableSet_allValue line 294
27. theorem OAI.InfiniteConditioning.allValue_probability line 298
28. theorem OAI.InfiniteConditioning.allValue_probability_constant line 302
29. theorem OAI.InfiniteConditioning.fixed_determined_probability line 311

    Source documentation

    A reveal has no effect on any observable determined by disjoint bits.

    theorem fixed_determined_probability (p : E → Set.Icc (0 : ℝ) 1)
        (J K : Finset E) (hJK : Disjoint J K) (ξ : E → Bool) (A : Set (E → Bool))
        (hA : ProductCylinder.DeterminedBy (F := Prop) K (fun ω => ω ∈ A)) :
    …

    Mentions: OAI.ProductCylinder.DeterminedBy

30. theorem OAI.InfiniteConditioning.ae_fixed_pattern line 328
31. theorem OAI.InfiniteConditioning.ae_fixed_determined line 336

    Source documentation

    On a fixed revealed pattern, every J-determined quantity is constant.

    theorem ae_fixed_determined {F : Sort uF} (p : E → Set.Icc (0 : ℝ) 1)
        (J : Finset E) (ξ : E → Bool) (f : (E → Bool) → F)
        (hf : ∀ ω ω', (∀ e ∈ J, ω' e = ω e) → f ω' = f ω) :
        ∀ᵐ ω ∂ProductCylinder.law (fixedParameter p J ξ), f ω = f ξ := by
    …

    Mentions: OAI.ProductCylinder.law, OAI.InfiniteConditioning.fixedParameter

32. theorem OAI.InfiniteConditioning.select_probability_le line 349
33. theorem OAI.InfiniteConditioning.select_probability_lower line 362

    Source documentation

    Exact lower bound after a selected reveal; null histories are included.

    theorem select_probability_lower (p : E → Set.Icc (0 : ℝ) 1) (J : Finset E)
        (P : (J → Bool) → Prop) (A : (J → Bool) → Set (E → Bool))
        (hA : ∀ a, MeasurableSet (A a)) {b : ℝ}
        (hb : ∀ a, P a → b ≤
          (ProductCylinder.law (fixedParameter p J (ProductCylinder.extend J a))).real (A a)) :
        b * (ProductCylinder.law p).real {ω | P (J.restrict ω)} ≤
          (ProductCylinder.law p).real {ω | P (J.restrict ω) ∧ ω ∈ A (J.restrict ω)} := by
    …

    Mentions: OAI.ProductCylinder.law, OAI.InfiniteConditioning.fixedParameter, OAI.ProductCylinder.extend