dchrvmasumif

Description: An asymptotic approximation for the sum of X ( n ) Lam ( n ) / n conditional on the value of the infinite sum S . (We will later show that the case S = 0 is impossible, and hence establish dchrvmasum .) (Contributed by Mario Carneiro, 5-May-2016)

	Ref	Expression
Hypotheses	rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
	rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
	rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	rpvmasum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
	rpvmasum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
	rpvmasum.1	⊢ 1 = ( 0_g ‘ 𝐺 )
	dchrisum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
	dchrisum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
	dchrvmasumif.f	⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
	dchrvmasumif.c	⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
	dchrvmasumif.s	⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑆 )
	dchrvmasumif.1	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / 𝑦 ) )
Assertion	dchrvmasumif	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) )

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2		rpvmasum.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3		rpvmasum.a	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		rpvmasum.g	⊢ 𝐺 = ( DChr ‘ 𝑁 )
5		rpvmasum.d	⊢ 𝐷 = ( Base ‘ 𝐺 )
6		rpvmasum.1	⊢ 1 = ( 0_g ‘ 𝐺 )
7		dchrisum.b	⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8		dchrisum.n1	⊢ ( 𝜑 → 𝑋 ≠ 1 )
9		dchrvmasumif.f	⊢ 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) / 𝑎 ) )
10		dchrvmasumif.c	⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
11		dchrvmasumif.s	⊢ ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑆 )
12		dchrvmasumif.1	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / 𝑦 ) )
13		eqid	⊢ ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) )
14	1 2 3 4 5 6 7 8 13	dchrvmasumlema	⊢ ( 𝜑 → ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) )
15	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → 𝑁 ∈ ℕ )
16	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → 𝑋 ∈ 𝐷 )
17	8	adantr	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → 𝑋 ≠ 1 )
18	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → 𝐶 ∈ ( 0 [,) +∞ ) )
19	11	adantr	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → seq 1 ( + , 𝐹 ) ⇝ 𝑆 )
20	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑆 ) ) ≤ ( 𝐶 / 𝑦 ) )
21		simprl	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → 𝑐 ∈ ( 0 [,) +∞ ) )
22		simprrl	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 )
23		simprrr	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) )
24	1 2 15 4 5 6 16 17 9 18 19 20 13 21 22 23	dchrvmasumiflem2	⊢ ( ( 𝜑 ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) ) ) → ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) )
25	24	rexlimdvaa	⊢ ( 𝜑 → ( ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) → ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) ) )
26	25	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑡 ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 3 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑎 ) ) · ( ( log ‘ 𝑎 ) / 𝑎 ) ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 · ( ( log ‘ 𝑦 ) / 𝑦 ) ) ) → ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) ) )
27	14 26	mpd	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ⁺ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑆 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) )

Metamath Proof Explorer

Theorem dchrvmasumif

Proof