ProbabilityTheory.cond_cond_eq_cond_inter
theorem ProbabilityTheory.cond_cond_eq_cond_inter :
∀ {Ω : Type u_1} {m : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) {s t : Set Ω}
[inst : MeasureTheory.IsFiniteMeasure μ],
MeasurableSet s →
MeasurableSet t → ProbabilityTheory.cond (ProbabilityTheory.cond μ s) t = ProbabilityTheory.cond μ (s ∩ t)
The theorem `ProbabilityTheory.cond_cond_eq_cond_inter` states that for a given measure space `Ω` with a measurable space `m` and a measure `μ`, and any two sets `s` and `t` in `Ω` that are measurable, conditioning first on `s` and then on `t` leads to the same measure as directly conditioning on the intersection of `s` and `t`. In other words, the conditional probability measure of `μ` on `s` followed by `t` equals the conditional probability measure of `μ` on the intersection of `s` and `t`. This corresponds to the intuition from probability theory that conditioning on two events in sequence is the same as conditioning on both events simultaneously.
More concisely: For any measure space `(Ω, Σ, m, μ)`, measurable sets `s` and `t` in `Σ`, `μ(s ∩ t | s) = μ(s ∩ t) / μ(s)` and `μ(s | s ∩ t) = μ(s ∩ t) / μ(t)`, hence `μ(s ∩ t | s) = μ(s | s ∩ t)`.
|
ProbabilityTheory.cond_apply
theorem ProbabilityTheory.cond_apply :
∀ {Ω : Type u_1} {m : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) {s : Set Ω},
MeasurableSet s → ∀ (t : Set Ω), ↑↑(ProbabilityTheory.cond μ s) t = (↑↑μ s)⁻¹ * ↑↑μ (s ∩ t)
This theorem pertains to the axiomatic definition of conditional probability derived from a measure-theoretic one. Given a measurable space Ω, a measure μ on that space, and a measurable set s, the theorem states that for any set t, the application of the conditional probability measure of μ on s to t equals the measure of the intersection of s and t multiplied by the inverse of the measure of s. In mathematical terms, this is equivalent to saying that the conditional probability of t given s, represented as `(ProbabilityTheory.cond μ s) t`, is equal to `μ(s ∩ t) / μ(s)`.
More concisely: The theorem asserts that for a measurable space Ω with measure μ, the conditional probability of a measurable set t given s is equal to the ratio of their intersection's measure to s's measure: `(ProbabilityTheory.cond μ s) t = μ(s ∩ t) / μ(s)`.
|
ProbabilityTheory.cond_isProbabilityMeasure
theorem ProbabilityTheory.cond_isProbabilityMeasure :
∀ {Ω : Type u_1} {m : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) {s : Set Ω}
[inst : MeasureTheory.IsFiniteMeasure μ],
↑↑μ s ≠ 0 → MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.cond μ s)
This theorem states that given any finite measure `μ` and any set `s` of positive measure in a measurable space, the conditional probability measure of `μ` on `set s` is a probability measure. The condition `↑↑μ s ≠ 0` ensures that the set `s` has positive measure. In other words, if we restrict our measure to a subset `s` and scale it by the inverse of its measure on `s` (which is the definition of a conditional probability measure), the resulting measure is a probability measure, given that the original measure was finite and the set `s` was of positive measure.
More concisely: Given a finite measure `μ` and a set `s` of positive measure in a measurable space, the restriction of `μ` to `s` and scalings by the inverse of `μ(s)` results in a probability measure.
|
ProbabilityTheory.cond_add_cond_compl_eq
theorem ProbabilityTheory.cond_add_cond_compl_eq :
∀ {Ω : Type u_1} {m : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) {s t : Set Ω}
[inst : MeasureTheory.IsFiniteMeasure μ],
MeasurableSet s → ↑↑(ProbabilityTheory.cond μ s) t * ↑↑μ s + ↑↑(ProbabilityTheory.cond μ sᶜ) t * ↑↑μ sᶜ = ↑↑μ t
This theorem represents a version of the law of total probability in the context of measure theory. It states that for any measurable space `Ω` with a finite measure `μ` and any two subsets `s` and `t` of `Ω` where `s` is a measurable set, the sum of the conditional probability of `t` given `s`, scaled by the measure of `s`, and the conditional probability of `t` given the complement of `s`, scaled by the measure of the complement of `s`, equals the measure of `t`. In notation, `(μ(s)⁻¹ * μ(t ∩ s)) * μ(s) + (μ(sᶜ)⁻¹ * μ(t ∩ sᶜ)) * μ(sᶜ) = μ(t)`.
More concisely: For any measurable spaces `(Ω, Σ)` with finite measure `μ`, and measurable sets `s` and `t` such that `s` is measurable and `μ(s) > 0`, the law of total probability holds: `μ(t) = μ(t ∩ s) / μ(s) + μ(t ∩ sᶜ) / μ(sᶜ)`.
|
ProbabilityTheory.cond_eq_inv_mul_cond_mul
theorem ProbabilityTheory.cond_eq_inv_mul_cond_mul :
∀ {Ω : Type u_1} {m : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) {s t : Set Ω}
[inst : MeasureTheory.IsFiniteMeasure μ],
MeasurableSet s →
MeasurableSet t → ↑↑(ProbabilityTheory.cond μ s) t = (↑↑μ s)⁻¹ * ↑↑(ProbabilityTheory.cond μ t) s * ↑↑μ t
**Bayes' Theorem**: For any type `Ω` equipped with a `MeasurableSpace` structure and a finite `MeasureTheory.Measure` `μ`, and any two measurable sets `s` and `t`, the conditional probability of `t` given `s` under measure `μ` is equal to the inverse of the measure of `s` times the conditional probability of `s` given `t` under measure `μ` times the measure of `t`. This is expressed mathematically as:
```
P(T|S) = (1/P(S)) * P(S|T) * P(T)
```
where `P(T|S)` is the conditional probability of `t` given `s`, `P(S)` is the measure of `s`, `P(S|T)` is the conditional probability of `s` given `t`, and `P(T)` is the measure of `t`.
More concisely: The conditional probability of `t` given `s` under measure `μ` is equal to the ratio of the conditional probability of `s` given `t` and the measure of `s`. That is, `P(T|S) = P(S|T) / P(S)`.
|