snmlflim

Description: If A is simply normal, then the function F of relative density of B in the digit string converges to 1 / R , i.e. the set of occurrences of B in the digit string has natural density 1 / R . (Contributed by Mario Carneiro, 6-Apr-2015)

	Ref	Expression
Hypotheses	snml.s	$⊢ S = (r \in ℤ_{\geq 2} ⟼ \{x \in ℝ \| \forall b \in (0 \dots r - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x r^{k} \mod r⌋ = b\}\|}{n}) ⇝ (\frac{1}{r})\})$
	snml.f	$⊢ F = (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|}{n})$
Assertion	snmlflim	$⊢ (A \in S (R) \land B \in (0 \dots R - 1)) \to F ⇝ (\frac{1}{R})$

Proof

Step	Hyp	Ref	Expression
1		snml.s	$⊢ S = (r \in ℤ_{\geq 2} ⟼ \{x \in ℝ \| \forall b \in (0 \dots r - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊x r^{k} \mod r⌋ = b\}\|}{n}) ⇝ (\frac{1}{r})\})$
2		snml.f	$⊢ F = (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|}{n})$
3	1	snmlval	$⊢ A \in S (R) \leftrightarrow (R \in ℤ_{\geq 2} \land A \in ℝ \land \forall b \in (0 \dots R - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R}))$
4	3	simp3bi	$⊢ A \in S (R) \to \forall b \in (0 \dots R - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R})$
5		eqeq2	$⊢ b = B \to (⌊A R^{k} \mod R⌋ = b \leftrightarrow ⌊A R^{k} \mod R⌋ = B)$
6	5	rabbidv	$⊢ b = B \to \{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\} = \{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}$
7	6	fveq2d	$⊢ b = B \to \|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\| = \|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|$
8	7	oveq1d	$⊢ b = B \to \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|}{n} = \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|}{n}$
9	8	mpteq2dv	$⊢ b = B \to (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|}{n}) = (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = B\}\|}{n})$
10	9 2	eqtr4di	$⊢ b = B \to (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|}{n}) = F$
11	10	breq1d	$⊢ b = B \to ((n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R}) \leftrightarrow F ⇝ (\frac{1}{R}))$
12	11	rspccva	$⊢ (\forall b \in (0 \dots R - 1) (n \in ℕ ⟼ \frac{\|\{k \in (1 \dots n) \| ⌊A R^{k} \mod R⌋ = b\}\|}{n}) ⇝ (\frac{1}{R}) \land B \in (0 \dots R - 1)) \to F ⇝ (\frac{1}{R})$
13	4 12	sylan	$⊢ (A \in S (R) \land B \in (0 \dots R - 1)) \to F ⇝ (\frac{1}{R})$

Metamath Proof Explorer

Theorem snmlflim

Proof