`BookProof.SqueezedGaussStates.tendsto_boundary` (ρ : ℝ) (h0 : 0 ≤ ρ) (h1 : ρ < 1) : Filter.Tendsto (fun M : ℕ => (2 * (M : ℝ) + 1) * ρ ^ M) Filter.atTop (nhds 0)

Initializing...

`BookProof.SqueezedGaussStates.tendsto_boundary` (ρ : ℝ) (h0 : 0 ≤ ρ) (h1 : ρ < 1) : Filter.Tendsto (fun M : ℕ => (2 * (M : ℝ) + 1) * ρ ^ M) Filter.atTop (nhds 0) · Prove2Me