![]() |
Metamath
Proof Explorer Theorem List (p. 345 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | probdif 34401 | The probability of the difference of two event sets. (Contributed by Thierry Arnoux, 12-Dec-2016.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → (𝑃‘(𝐴 ∖ 𝐵)) = ((𝑃‘𝐴) − (𝑃‘(𝐴 ∩ 𝐵)))) | ||
Theorem | probinc 34402 | A probability law is increasing with regard to event set inclusion. (Contributed by Thierry Arnoux, 10-Feb-2017.) |
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ 𝐴 ⊆ 𝐵) → (𝑃‘𝐴) ≤ (𝑃‘𝐵)) | ||
Theorem | probdsb 34403 | The probability of the complement of a set. That is, the probability that the event 𝐴 does not occur. (Contributed by Thierry Arnoux, 15-Dec-2016.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃) → (𝑃‘(∪ dom 𝑃 ∖ 𝐴)) = (1 − (𝑃‘𝐴))) | ||
Theorem | probmeasd 34404 | A probability measure is a measure. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) ⇒ ⊢ (𝜑 → 𝑃 ∈ ∪ ran measures) | ||
Theorem | probvalrnd 34405 | The value of a probability is a real number. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑃) ⇒ ⊢ (𝜑 → (𝑃‘𝐴) ∈ ℝ) | ||
Theorem | probtotrnd 34406 | The probability of the universe set is finite. (Contributed by Thierry Arnoux, 2-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) ⇒ ⊢ (𝜑 → (𝑃‘∪ dom 𝑃) ∈ ℝ) | ||
Theorem | totprobd 34407* | Law of total probability, deduction form. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝐴 ∈ dom 𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝒫 dom 𝑃) & ⊢ (𝜑 → ∪ 𝐵 = ∪ dom 𝑃) & ⊢ (𝜑 → 𝐵 ≼ ω) & ⊢ (𝜑 → Disj 𝑏 ∈ 𝐵 𝑏) ⇒ ⊢ (𝜑 → (𝑃‘𝐴) = Σ*𝑏 ∈ 𝐵(𝑃‘(𝑏 ∩ 𝐴))) | ||
Theorem | totprob 34408* | Law of total probability. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ (∪ 𝐵 = ∪ dom 𝑃 ∧ 𝐵 ∈ 𝒫 dom 𝑃 ∧ (𝐵 ≼ ω ∧ Disj 𝑏 ∈ 𝐵 𝑏))) → (𝑃‘𝐴) = Σ*𝑏 ∈ 𝐵(𝑃‘(𝑏 ∩ 𝐴))) | ||
Theorem | probfinmeasb 34409 | Build a probability measure from a finite measure. (Contributed by Thierry Arnoux, 31-Jan-2017.) |
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝑀‘∪ 𝑆) ∈ ℝ+) → (𝑀 ∘f/c /𝑒 (𝑀‘∪ 𝑆)) ∈ Prob) | ||
Theorem | probfinmeasbALTV 34410* | Alternate version of probfinmeasb 34409. (Contributed by Thierry Arnoux, 17-Dec-2016.) (New usage is discouraged.) |
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ (𝑀‘∪ 𝑆) ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘𝑥) /𝑒 (𝑀‘∪ 𝑆))) ∈ Prob) | ||
Theorem | probmeasb 34411* | Build a probability from a measure and a set with finite measure. (Contributed by Thierry Arnoux, 25-Dec-2016.) |
⊢ ((𝑀 ∈ (measures‘𝑆) ∧ 𝐴 ∈ 𝑆 ∧ (𝑀‘𝐴) ∈ ℝ+) → (𝑥 ∈ 𝑆 ↦ ((𝑀‘(𝑥 ∩ 𝐴)) / (𝑀‘𝐴))) ∈ Prob) | ||
Syntax | ccprob 34412 | Extends class notation with the conditional probability builder. |
class cprob | ||
Definition | df-cndprob 34413* | Define the conditional probability. (Contributed by Thierry Arnoux, 14-Sep-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
⊢ cprob = (𝑝 ∈ Prob ↦ (𝑎 ∈ dom 𝑝, 𝑏 ∈ dom 𝑝 ↦ ((𝑝‘(𝑎 ∩ 𝑏)) / (𝑝‘𝑏)))) | ||
Theorem | cndprobval 34414 | The value of the conditional probability , i.e. the probability for the event 𝐴, given 𝐵, under the probability law 𝑃. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) → ((cprob‘𝑃)‘〈𝐴, 𝐵〉) = ((𝑃‘(𝐴 ∩ 𝐵)) / (𝑃‘𝐵))) | ||
Theorem | cndprobin 34415 | An identity linking conditional probability and intersection. (Contributed by Thierry Arnoux, 13-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑃‘𝐵) ≠ 0) → (((cprob‘𝑃)‘〈𝐴, 𝐵〉) · (𝑃‘𝐵)) = (𝑃‘(𝐴 ∩ 𝐵))) | ||
Theorem | cndprob01 34416 | The conditional probability has values in [0, 1]. (Contributed by Thierry Arnoux, 13-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑃‘𝐵) ≠ 0) → ((cprob‘𝑃)‘〈𝐴, 𝐵〉) ∈ (0[,]1)) | ||
Theorem | cndprobtot 34417 | The conditional probability given a certain event is one. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ (𝑃‘𝐴) ≠ 0) → ((cprob‘𝑃)‘〈∪ dom 𝑃, 𝐴〉) = 1) | ||
Theorem | cndprobnul 34418 | The conditional probability given empty event is zero. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ (𝑃‘𝐴) ≠ 0) → ((cprob‘𝑃)‘〈∅, 𝐴〉) = 0) | ||
Theorem | cndprobprob 34419* | The conditional probability defines a probability law. (Contributed by Thierry Arnoux, 23-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
⊢ ((𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ∧ (𝑃‘𝐵) ≠ 0) → (𝑎 ∈ dom 𝑃 ↦ ((cprob‘𝑃)‘〈𝑎, 𝐵〉)) ∈ Prob) | ||
Theorem | bayesth 34420 | Bayes Theorem. (Contributed by Thierry Arnoux, 20-Dec-2016.) (Revised by Thierry Arnoux, 21-Jan-2017.) |
⊢ (((𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃) ∧ (𝑃‘𝐴) ≠ 0 ∧ (𝑃‘𝐵) ≠ 0) → ((cprob‘𝑃)‘〈𝐴, 𝐵〉) = ((((cprob‘𝑃)‘〈𝐵, 𝐴〉) · (𝑃‘𝐴)) / (𝑃‘𝐵))) | ||
Syntax | crrv 34421 | Extend class notation with the class of real-valued random variables. |
class rRndVar | ||
Definition | df-rrv 34422 | In its generic definition, a random variable is a measurable function from a probability space to a Borel set. Here, we specifically target real-valued random variables, i.e. measurable function from a probability space to the Borel sigma-algebra on the set of real numbers. (Contributed by Thierry Arnoux, 20-Sep-2016.) (Revised by Thierry Arnoux, 25-Jan-2017.) |
⊢ rRndVar = (𝑝 ∈ Prob ↦ (dom 𝑝MblFnM𝔅ℝ)) | ||
Theorem | rrvmbfm 34423 | A real-valued random variable is a measurable function from its sample space to the Borel sigma-algebra. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) ⇒ ⊢ (𝜑 → (𝑋 ∈ (rRndVar‘𝑃) ↔ 𝑋 ∈ (dom 𝑃MblFnM𝔅ℝ))) | ||
Theorem | isrrvv 34424* | Elementhood to the set of real-valued random variables with respect to the probability 𝑃. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) ⇒ ⊢ (𝜑 → (𝑋 ∈ (rRndVar‘𝑃) ↔ (𝑋:∪ dom 𝑃⟶ℝ ∧ ∀𝑦 ∈ 𝔅ℝ (◡𝑋 “ 𝑦) ∈ dom 𝑃))) | ||
Theorem | rrvvf 34425 | A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → 𝑋:∪ dom 𝑃⟶ℝ) | ||
Theorem | rrvfn 34426 | A real-valued random variable is a function over the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → 𝑋 Fn ∪ dom 𝑃) | ||
Theorem | rrvdm 34427 | The domain of a random variable is the universe. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → dom 𝑋 = ∪ dom 𝑃) | ||
Theorem | rrvrnss 34428 | The range of a random variable as a subset of ℝ. (Contributed by Thierry Arnoux, 6-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → ran 𝑋 ⊆ ℝ) | ||
Theorem | rrvf2 34429 | A real-valued random variable is a function. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → 𝑋:dom 𝑋⟶ℝ) | ||
Theorem | rrvdmss 34430 | The domain of a random variable. This is useful to shorten proofs. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → ∪ dom 𝑃 ⊆ dom 𝑋) | ||
Theorem | rrvfinvima 34431* | For a real-value random variable 𝑋, any open interval in ℝ is the image of a measurable set. (Contributed by Thierry Arnoux, 25-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → ∀𝑦 ∈ 𝔅ℝ (◡𝑋 “ 𝑦) ∈ dom 𝑃) | ||
Theorem | 0rrv 34432* | The constant function equal to zero is a random variable. (Contributed by Thierry Arnoux, 16-Jan-2017.) (Revised by Thierry Arnoux, 30-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) ⇒ ⊢ (𝜑 → (𝑥 ∈ ∪ dom 𝑃 ↦ 0) ∈ (rRndVar‘𝑃)) | ||
Theorem | rrvadd 34433 | The sum of two random variables is a random variable. (Contributed by Thierry Arnoux, 4-Jun-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝑌 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → (𝑋 ∘f + 𝑌) ∈ (rRndVar‘𝑃)) | ||
Theorem | rrvmulc 34434 | A random variable multiplied by a constant is a random variable. (Contributed by Thierry Arnoux, 17-Jan-2017.) (Revised by Thierry Arnoux, 22-May-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐶 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑋 ∘f/c · 𝐶) ∈ (rRndVar‘𝑃)) | ||
Theorem | rrvsum 34435 | An indexed sum of random variables is a random variable. (Contributed by Thierry Arnoux, 22-May-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋:ℕ⟶(rRndVar‘𝑃)) & ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑆 = (seq1( ∘f + , 𝑋)‘𝑁)) ⇒ ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ) → 𝑆 ∈ (rRndVar‘𝑃)) | ||
Syntax | corvc 34436 | Extend class notation to include the preimage set mapping operator. |
class ∘RV/𝑐𝑅 | ||
Definition | df-orvc 34437* |
Define the preimage set mapping operator. In probability theory, the
notation 𝑃(𝑋 = 𝐴) denotes the probability that a
random variable
𝑋 takes the value 𝐴. We
introduce here an operator which
enables to write this in Metamath as (𝑃‘(𝑋∘RV/𝑐 I 𝐴)), and
keep a similar notation. Because with this notation (𝑋∘RV/𝑐 I 𝐴)
is a set, we can also apply it to conditional probabilities, like in
(𝑃‘(𝑋∘RV/𝑐 I 𝐴) ∣ (𝑌∘RV/𝑐 I 𝐵))).
The oRVC operator transforms a relation 𝑅 into an operation taking a random variable 𝑋 and a constant 𝐶, and returning the preimage through 𝑋 of the equivalence class of 𝐶. The most commonly used relations are: - equality: {𝑋 = 𝐴} as (𝑋∘RV/𝑐 I 𝐴) cf. ideq 5865- elementhood: {𝑋 ∈ 𝐴} as (𝑋∘RV/𝑐 E 𝐴) cf. epel 5591- less-than: {𝑋 ≤ 𝐴} as (𝑋∘RV/𝑐 ≤ 𝐴) Even though it is primarily designed to be used within probability theory and with random variables, this operator is defined on generic functions, and could be used in other fields, e.g., for continuous functions. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
⊢ ∘RV/𝑐𝑅 = (𝑥 ∈ {𝑥 ∣ Fun 𝑥}, 𝑎 ∈ V ↦ (◡𝑥 “ {𝑦 ∣ 𝑦𝑅𝑎})) | ||
Theorem | orvcval 34438* | Value of the preimage mapping operator applied on a given random variable and constant. (Contributed by Thierry Arnoux, 19-Jan-2017.) |
⊢ (𝜑 → Fun 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) = (◡𝑋 “ {𝑦 ∣ 𝑦𝑅𝐴})) | ||
Theorem | orvcval2 34439* | Another way to express the value of the preimage mapping operator. (Contributed by Thierry Arnoux, 19-Jan-2017.) |
⊢ (𝜑 → Fun 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) = {𝑧 ∈ dom 𝑋 ∣ (𝑋‘𝑧)𝑅𝐴}) | ||
Theorem | elorvc 34440* | Elementhood of a preimage. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → Fun 𝑋) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) ⇒ ⊢ ((𝜑 ∧ 𝑧 ∈ dom 𝑋) → (𝑧 ∈ (𝑋∘RV/𝑐𝑅𝐴) ↔ (𝑋‘𝑧)𝑅𝐴)) | ||
Theorem | orvcval4 34441* | The value of the preimage mapping operator can be restricted to preimages in the base set of the topology. Cf. orvcval 34438. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑋 ∈ (𝑆MblFnM(sigaGen‘𝐽))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) = (◡𝑋 “ {𝑦 ∈ ∪ 𝐽 ∣ 𝑦𝑅𝐴})) | ||
Theorem | orvcoel 34442* | If the relation produces open sets, preimage maps by a measurable function are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑋 ∈ (𝑆MblFnM(sigaGen‘𝐽))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → {𝑦 ∈ ∪ 𝐽 ∣ 𝑦𝑅𝐴} ∈ 𝐽) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) ∈ 𝑆) | ||
Theorem | orvccel 34443* | If the relation produces closed sets, preimage maps by a measurable function are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → 𝑆 ∈ ∪ ran sigAlgebra) & ⊢ (𝜑 → 𝐽 ∈ Top) & ⊢ (𝜑 → 𝑋 ∈ (𝑆MblFnM(sigaGen‘𝐽))) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → {𝑦 ∈ ∪ 𝐽 ∣ 𝑦𝑅𝐴} ∈ (Clsd‘𝐽)) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) ∈ 𝑆) | ||
Theorem | elorrvc 34444* | Elementhood of a preimage for a real-valued random variable. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ dom 𝑃) → (𝑧 ∈ (𝑋∘RV/𝑐𝑅𝐴) ↔ (𝑋‘𝑧)𝑅𝐴)) | ||
Theorem | orrvcval4 34445* | The value of the preimage mapping operator can be restricted to preimages of subsets of ℝ. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) = (◡𝑋 “ {𝑦 ∈ ℝ ∣ 𝑦𝑅𝐴})) | ||
Theorem | orrvcoel 34446* | If the relation produces open sets, preimage maps of a random variable are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → {𝑦 ∈ ℝ ∣ 𝑦𝑅𝐴} ∈ (topGen‘ran (,))) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) ∈ dom 𝑃) | ||
Theorem | orrvccel 34447* | If the relation produces closed sets, preimage maps are measurable sets. (Contributed by Thierry Arnoux, 21-Jan-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → {𝑦 ∈ ℝ ∣ 𝑦𝑅𝐴} ∈ (Clsd‘(topGen‘ran (,)))) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐𝑅𝐴) ∈ dom 𝑃) | ||
Theorem | orvcgteel 34448 | Preimage maps produced by the "greater than or equal to" relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐◡ ≤ 𝐴) ∈ dom 𝑃) | ||
Theorem | orvcelval 34449 | Preimage maps produced by the membership relation. (Contributed by Thierry Arnoux, 6-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ 𝔅ℝ) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐 E 𝐴) = (◡𝑋 “ 𝐴)) | ||
Theorem | orvcelel 34450 | Preimage maps produced by the membership relation are measurable sets. (Contributed by Thierry Arnoux, 5-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ 𝔅ℝ) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐 E 𝐴) ∈ dom 𝑃) | ||
Theorem | dstrvval 34451* | The value of the distribution of a random variable. (Contributed by Thierry Arnoux, 9-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐷 = (𝑎 ∈ 𝔅ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 E 𝑎)))) & ⊢ (𝜑 → 𝐴 ∈ 𝔅ℝ) ⇒ ⊢ (𝜑 → (𝐷‘𝐴) = (𝑃‘(◡𝑋 “ 𝐴))) | ||
Theorem | dstrvprob 34452* | The distribution of a random variable is a probability law. (TODO: could be shortened using dstrvval 34451). (Contributed by Thierry Arnoux, 10-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐷 = (𝑎 ∈ 𝔅ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 E 𝑎)))) ⇒ ⊢ (𝜑 → 𝐷 ∈ Prob) | ||
Theorem | orvclteel 34453 | Preimage maps produced by the "less than or equal to" relation are measurable sets. (Contributed by Thierry Arnoux, 4-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐 ≤ 𝐴) ∈ dom 𝑃) | ||
Theorem | dstfrvel 34454 | Elementhood of preimage maps produced by the "less than or equal to" relation. (Contributed by Thierry Arnoux, 13-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ∪ dom 𝑃) & ⊢ (𝜑 → (𝑋‘𝐵) ≤ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ∈ (𝑋∘RV/𝑐 ≤ 𝐴)) | ||
Theorem | dstfrvunirn 34455* | The limit of all preimage maps by the "less than or equal to" relation is the universe. (Contributed by Thierry Arnoux, 12-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) ⇒ ⊢ (𝜑 → ∪ ran (𝑛 ∈ ℕ ↦ (𝑋∘RV/𝑐 ≤ 𝑛)) = ∪ dom 𝑃) | ||
Theorem | orvclteinc 34456 | Preimage maps produced by the "less than or equal to" relation are increasing. (Contributed by Thierry Arnoux, 11-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝑋∘RV/𝑐 ≤ 𝐴) ⊆ (𝑋∘RV/𝑐 ≤ 𝐵)) | ||
Theorem | dstfrvinc 34457* | A cumulative distribution function is nondecreasing. (Contributed by Thierry Arnoux, 11-Feb-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥)))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐴 ≤ 𝐵) ⇒ ⊢ (𝜑 → (𝐹‘𝐴) ≤ (𝐹‘𝐵)) | ||
Theorem | dstfrvclim1 34458* | The limit of the cumulative distribution function is one. (Contributed by Thierry Arnoux, 12-Feb-2017.) (Revised by Thierry Arnoux, 11-Jul-2017.) |
⊢ (𝜑 → 𝑃 ∈ Prob) & ⊢ (𝜑 → 𝑋 ∈ (rRndVar‘𝑃)) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝑃‘(𝑋∘RV/𝑐 ≤ 𝑥)))) ⇒ ⊢ (𝜑 → 𝐹 ⇝ 1) | ||
Theorem | coinfliplem 34459 | Division in the extended real numbers can be used for the coin-flip example. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
⊢ 𝐻 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝐻 ≠ 𝑇 & ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c / 2) & ⊢ 𝑋 = {〈𝐻, 1〉, 〈𝑇, 0〉} ⇒ ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c /𝑒 2) | ||
Theorem | coinflipprob 34460 | The 𝑃 we defined for coin-flip is a probability law. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
⊢ 𝐻 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝐻 ≠ 𝑇 & ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c / 2) & ⊢ 𝑋 = {〈𝐻, 1〉, 〈𝑇, 0〉} ⇒ ⊢ 𝑃 ∈ Prob | ||
Theorem | coinflipspace 34461 | The space of our coin-flip probability. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
⊢ 𝐻 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝐻 ≠ 𝑇 & ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c / 2) & ⊢ 𝑋 = {〈𝐻, 1〉, 〈𝑇, 0〉} ⇒ ⊢ dom 𝑃 = 𝒫 {𝐻, 𝑇} | ||
Theorem | coinflipuniv 34462 | The universe of our coin-flip probability is {𝐻, 𝑇}. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
⊢ 𝐻 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝐻 ≠ 𝑇 & ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c / 2) & ⊢ 𝑋 = {〈𝐻, 1〉, 〈𝑇, 0〉} ⇒ ⊢ ∪ dom 𝑃 = {𝐻, 𝑇} | ||
Theorem | coinfliprv 34463 | The 𝑋 we defined for coin-flip is a random variable. (Contributed by Thierry Arnoux, 12-Jan-2017.) |
⊢ 𝐻 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝐻 ≠ 𝑇 & ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c / 2) & ⊢ 𝑋 = {〈𝐻, 1〉, 〈𝑇, 0〉} ⇒ ⊢ 𝑋 ∈ (rRndVar‘𝑃) | ||
Theorem | coinflippv 34464 | The probability of heads is one-half. (Contributed by Thierry Arnoux, 15-Jan-2017.) |
⊢ 𝐻 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝐻 ≠ 𝑇 & ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c / 2) & ⊢ 𝑋 = {〈𝐻, 1〉, 〈𝑇, 0〉} ⇒ ⊢ (𝑃‘{𝐻}) = (1 / 2) | ||
Theorem | coinflippvt 34465 | The probability of tails is one-half. (Contributed by Thierry Arnoux, 5-Feb-2017.) |
⊢ 𝐻 ∈ V & ⊢ 𝑇 ∈ V & ⊢ 𝐻 ≠ 𝑇 & ⊢ 𝑃 = ((♯ ↾ 𝒫 {𝐻, 𝑇}) ∘f/c / 2) & ⊢ 𝑋 = {〈𝐻, 1〉, 〈𝑇, 0〉} ⇒ ⊢ (𝑃‘{𝑇}) = (1 / 2) | ||
Theorem | ballotlemoex 34466* | 𝑂 is a set. (Contributed by Thierry Arnoux, 7-Dec-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} ⇒ ⊢ 𝑂 ∈ V | ||
Theorem | ballotlem1 34467* | The size of the universe is a binomial coefficient. (Contributed by Thierry Arnoux, 23-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} ⇒ ⊢ (♯‘𝑂) = ((𝑀 + 𝑁)C𝑀) | ||
Theorem | ballotlemelo 34468* | Elementhood in 𝑂. (Contributed by Thierry Arnoux, 17-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} ⇒ ⊢ (𝐶 ∈ 𝑂 ↔ (𝐶 ⊆ (1...(𝑀 + 𝑁)) ∧ (♯‘𝐶) = 𝑀)) | ||
Theorem | ballotlem2 34469* | The probability that the first vote picked in a count is a B. (Contributed by Thierry Arnoux, 23-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) ⇒ ⊢ (𝑃‘{𝑐 ∈ 𝑂 ∣ ¬ 1 ∈ 𝑐}) = (𝑁 / (𝑀 + 𝑁)) | ||
Theorem | ballotlemfval 34470* | The value of 𝐹. (Contributed by Thierry Arnoux, 23-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ (𝜑 → 𝐶 ∈ 𝑂) & ⊢ (𝜑 → 𝐽 ∈ ℤ) ⇒ ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) = ((♯‘((1...𝐽) ∩ 𝐶)) − (♯‘((1...𝐽) ∖ 𝐶)))) | ||
Theorem | ballotlemfelz 34471* | (𝐹‘𝐶) has values in ℤ. (Contributed by Thierry Arnoux, 23-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ (𝜑 → 𝐶 ∈ 𝑂) & ⊢ (𝜑 → 𝐽 ∈ ℤ) ⇒ ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) ∈ ℤ) | ||
Theorem | ballotlemfp1 34472* | If the 𝐽 th ballot is for A, (𝐹‘𝐶) goes up 1. If the 𝐽 th ballot is for B, (𝐹‘𝐶) goes down 1. (Contributed by Thierry Arnoux, 24-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ (𝜑 → 𝐶 ∈ 𝑂) & ⊢ (𝜑 → 𝐽 ∈ ℕ) ⇒ ⊢ (𝜑 → ((¬ 𝐽 ∈ 𝐶 → ((𝐹‘𝐶)‘𝐽) = (((𝐹‘𝐶)‘(𝐽 − 1)) − 1)) ∧ (𝐽 ∈ 𝐶 → ((𝐹‘𝐶)‘𝐽) = (((𝐹‘𝐶)‘(𝐽 − 1)) + 1)))) | ||
Theorem | ballotlemfc0 34473* | 𝐹 takes value 0 between negative and positive values. (Contributed by Thierry Arnoux, 24-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ (𝜑 → 𝐶 ∈ 𝑂) & ⊢ (𝜑 → 𝐽 ∈ ℕ) & ⊢ (𝜑 → ∃𝑖 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑖) ≤ 0) & ⊢ (𝜑 → 0 < ((𝐹‘𝐶)‘𝐽)) ⇒ ⊢ (𝜑 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0) | ||
Theorem | ballotlemfcc 34474* | 𝐹 takes value 0 between positive and negative values. (Contributed by Thierry Arnoux, 2-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ (𝜑 → 𝐶 ∈ 𝑂) & ⊢ (𝜑 → 𝐽 ∈ ℕ) & ⊢ (𝜑 → ∃𝑖 ∈ (1...𝐽)0 ≤ ((𝐹‘𝐶)‘𝑖)) & ⊢ (𝜑 → ((𝐹‘𝐶)‘𝐽) < 0) ⇒ ⊢ (𝜑 → ∃𝑘 ∈ (1...𝐽)((𝐹‘𝐶)‘𝑘) = 0) | ||
Theorem | ballotlemfmpn 34475* | (𝐹‘𝐶) finishes counting at (𝑀 − 𝑁). (Contributed by Thierry Arnoux, 25-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) ⇒ ⊢ (𝐶 ∈ 𝑂 → ((𝐹‘𝐶)‘(𝑀 + 𝑁)) = (𝑀 − 𝑁)) | ||
Theorem | ballotlemfval0 34476* | (𝐹‘𝐶) always starts counting at 0 . (Contributed by Thierry Arnoux, 25-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) ⇒ ⊢ (𝐶 ∈ 𝑂 → ((𝐹‘𝐶)‘0) = 0) | ||
Theorem | ballotleme 34477* | Elements of 𝐸. (Contributed by Thierry Arnoux, 14-Dec-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} ⇒ ⊢ (𝐶 ∈ 𝐸 ↔ (𝐶 ∈ 𝑂 ∧ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝐶)‘𝑖))) | ||
Theorem | ballotlemodife 34478* | Elements of (𝑂 ∖ 𝐸). (Contributed by Thierry Arnoux, 7-Dec-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) ↔ (𝐶 ∈ 𝑂 ∧ ∃𝑖 ∈ (1...(𝑀 + 𝑁))((𝐹‘𝐶)‘𝑖) ≤ 0)) | ||
Theorem | ballotlem4 34479* | If the first pick is a vote for B, A is not ahead throughout the count. (Contributed by Thierry Arnoux, 25-Nov-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} ⇒ ⊢ (𝐶 ∈ 𝑂 → (¬ 1 ∈ 𝐶 → ¬ 𝐶 ∈ 𝐸)) | ||
Theorem | ballotlem5 34480* | If A is not ahead throughout, there is a 𝑘 where votes are tied. (Contributed by Thierry Arnoux, 1-Dec-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ∃𝑘 ∈ (1...(𝑀 + 𝑁))((𝐹‘𝐶)‘𝑘) = 0) | ||
Theorem | ballotlemi 34481* | Value of 𝐼 for a given counting 𝐶. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝐼‘𝐶) = inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}, ℝ, < )) | ||
Theorem | ballotlemiex 34482* | Properties of (𝐼‘𝐶). (Contributed by Thierry Arnoux, 12-Dec-2016.) (Revised by AV, 6-Oct-2020.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝐼‘𝐶) ∈ (1...(𝑀 + 𝑁)) ∧ ((𝐹‘𝐶)‘(𝐼‘𝐶)) = 0)) | ||
Theorem | ballotlemi1 34483* | The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 12-Mar-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ ¬ 1 ∈ 𝐶) → (𝐼‘𝐶) ≠ 1) | ||
Theorem | ballotlemii 34484* | The first tie cannot be reached at the first pick. (Contributed by Thierry Arnoux, 4-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → (𝐼‘𝐶) ≠ 1) | ||
Theorem | ballotlemsup 34485* | The set of zeroes of 𝐹 satisfies the conditions to have a supremum. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ∃𝑧 ∈ ℝ (∀𝑤 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0} ¬ 𝑤 < 𝑧 ∧ ∀𝑤 ∈ ℝ (𝑧 < 𝑤 → ∃𝑦 ∈ {𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝐶)‘𝑘) = 0}𝑦 < 𝑤))) | ||
Theorem | ballotlemimin 34486* | (𝐼‘𝐶) is the first tie. (Contributed by Thierry Arnoux, 1-Dec-2016.) (Revised by AV, 6-Oct-2020.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ¬ ∃𝑘 ∈ (1...((𝐼‘𝐶) − 1))((𝐹‘𝐶)‘𝑘) = 0) | ||
Theorem | ballotlemic 34487* | If the first vote is for B, the vote on the first tie is for A. (Contributed by Thierry Arnoux, 1-Dec-2016.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ ¬ 1 ∈ 𝐶) → (𝐼‘𝐶) ∈ 𝐶) | ||
Theorem | ballotlem1c 34488* | If the first vote is for A, the vote on the first tie is for B. (Contributed by Thierry Arnoux, 4-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 1 ∈ 𝐶) → ¬ (𝐼‘𝐶) ∈ 𝐶) | ||
Theorem | ballotlemsval 34489* | Value of 𝑆. (Contributed by Thierry Arnoux, 12-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑆‘𝐶) = (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝐶), (((𝐼‘𝐶) + 1) − 𝑖), 𝑖))) | ||
Theorem | ballotlemsv 34490* | Value of 𝑆 evaluated at 𝐽 for a given counting 𝐶. (Contributed by Thierry Arnoux, 12-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → ((𝑆‘𝐶)‘𝐽) = if(𝐽 ≤ (𝐼‘𝐶), (((𝐼‘𝐶) + 1) − 𝐽), 𝐽)) | ||
Theorem | ballotlemsgt1 34491* | 𝑆 maps values less than (𝐼‘𝐶) to values greater than 1. (Contributed by Thierry Arnoux, 28-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁)) ∧ 𝐽 < (𝐼‘𝐶)) → 1 < ((𝑆‘𝐶)‘𝐽)) | ||
Theorem | ballotlemsdom 34492* | Domain of 𝑆 for a given counting 𝐶. (Contributed by Thierry Arnoux, 12-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → ((𝑆‘𝐶)‘𝐽) ∈ (1...(𝑀 + 𝑁))) | ||
Theorem | ballotlemsel1i 34493* | The range (1...(𝐼‘𝐶)) is invariant under (𝑆‘𝐶). (Contributed by Thierry Arnoux, 28-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶)‘𝐽) ∈ (1...(𝐼‘𝐶))) | ||
Theorem | ballotlemsf1o 34494* | The defined 𝑆 is a bijection, and an involution. (Contributed by Thierry Arnoux, 14-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝑆‘𝐶):(1...(𝑀 + 𝑁))–1-1-onto→(1...(𝑀 + 𝑁)) ∧ ◡(𝑆‘𝐶) = (𝑆‘𝐶))) | ||
Theorem | ballotlemsi 34495* | The image by 𝑆 of the first tie pick is the first pick. (Contributed by Thierry Arnoux, 14-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝑆‘𝐶)‘(𝐼‘𝐶)) = 1) | ||
Theorem | ballotlemsima 34496* | The image by 𝑆 of an interval before the first pick. (Contributed by Thierry Arnoux, 5-May-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝐼‘𝐶))) → ((𝑆‘𝐶) “ (1...𝐽)) = (((𝑆‘𝐶)‘𝐽)...(𝐼‘𝐶))) | ||
Theorem | ballotlemieq 34497* | If two countings share the same first tie, they also have the same swap function. (Contributed by Thierry Arnoux, 18-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐷 ∈ (𝑂 ∖ 𝐸) ∧ (𝐼‘𝐶) = (𝐼‘𝐷)) → (𝑆‘𝐶) = (𝑆‘𝐷)) | ||
Theorem | ballotlemrval 34498* | Value of 𝑅. (Contributed by Thierry Arnoux, 14-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) & ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐)) ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → (𝑅‘𝐶) = ((𝑆‘𝐶) “ 𝐶)) | ||
Theorem | ballotlemscr 34499* | The image of (𝑅‘𝐶) by (𝑆‘𝐶). (Contributed by Thierry Arnoux, 21-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) & ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐)) ⇒ ⊢ (𝐶 ∈ (𝑂 ∖ 𝐸) → ((𝑆‘𝐶) “ (𝑅‘𝐶)) = 𝐶) | ||
Theorem | ballotlemrv 34500* | Value of 𝑅 evaluated at 𝐽. (Contributed by Thierry Arnoux, 17-Apr-2017.) |
⊢ 𝑀 ∈ ℕ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑂 = {𝑐 ∈ 𝒫 (1...(𝑀 + 𝑁)) ∣ (♯‘𝑐) = 𝑀} & ⊢ 𝑃 = (𝑥 ∈ 𝒫 𝑂 ↦ ((♯‘𝑥) / (♯‘𝑂))) & ⊢ 𝐹 = (𝑐 ∈ 𝑂 ↦ (𝑖 ∈ ℤ ↦ ((♯‘((1...𝑖) ∩ 𝑐)) − (♯‘((1...𝑖) ∖ 𝑐))))) & ⊢ 𝐸 = {𝑐 ∈ 𝑂 ∣ ∀𝑖 ∈ (1...(𝑀 + 𝑁))0 < ((𝐹‘𝑐)‘𝑖)} & ⊢ 𝑁 < 𝑀 & ⊢ 𝐼 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ inf({𝑘 ∈ (1...(𝑀 + 𝑁)) ∣ ((𝐹‘𝑐)‘𝑘) = 0}, ℝ, < )) & ⊢ 𝑆 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ (𝑖 ∈ (1...(𝑀 + 𝑁)) ↦ if(𝑖 ≤ (𝐼‘𝑐), (((𝐼‘𝑐) + 1) − 𝑖), 𝑖))) & ⊢ 𝑅 = (𝑐 ∈ (𝑂 ∖ 𝐸) ↦ ((𝑆‘𝑐) “ 𝑐)) ⇒ ⊢ ((𝐶 ∈ (𝑂 ∖ 𝐸) ∧ 𝐽 ∈ (1...(𝑀 + 𝑁))) → (𝐽 ∈ (𝑅‘𝐶) ↔ if(𝐽 ≤ (𝐼‘𝐶), (((𝐼‘𝐶) + 1) − 𝐽), 𝐽) ∈ 𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |