1. FormalConjectures
  2. Books
  3. BugeaudDistributionModuloOne
  4. Problem10_6
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Bugeaud Collection of Conjectures and Open Questions: Rapidly Increasing Sequences Dense Modulo One

References:

    [Bos94] Boshernitzan, Michael D. "Density modulo 1 of dilations of sublacunary sequences." Advances in Mathematics 108.1 (1994): 104-117.

    [Bug12] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Vol. 193. Cambridge University Press, 2012. Chapter 10.

    [Fur67] Furstenberg, H. "Disjointness in ergodic theory, minimal sets, and a problem in diophantine approximation". Math. Systems Theory 1, 1–49 (1967).

    [Mat80] de Mathan, Bernard. "Numbers contravening a condition in density modulo 1." Acta Mathematica Hungarica 36.3-4 (1980): 237-241.

    [Pol79] Pollington, Andrew Douglas. "On the density of sequence ${n_ {k}\xi} $." Illinois Journal of Mathematics 23.4 (1979): 511-515.

namespace Bugeaud06 open Filter

The Pollington–de Mathan theorem [Pol79][Mat80]. For every lacunary sequence $(m_n){n \ge 1}$ of positive integers, the set of real numbers $\xi$ for which $({\xi m_n}){n \ge 1}$ is not dense modulo one has full Hausdorff dimension.

@[category research solved, AMS 11] theorem declaration uses 'sorry'pollington_de_mathan (m : ℕ → ℕ) (hm : ∀ n, 0 < m n) (hlac : IsLacunary m) : dimH {ξ : ℝ | ¬ Dense (Set.range fun n => (↑(ξ * m n) : AddCircle (1 : ℝ)))} = 1 := m:ℕ → ℕhm:∀ (n : ℕ), 0 < m nhlac:IsLacunary m⊢ dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m n)))} = 1 All goals completed! 🐙

The Pollington–de Mathan theorem implies that a lacunary sequence cannot answer Problem 10.6.

@[category test, AMS 11] theorem problem_lacunary_not_dense_of_pollington_de_mathan (h : type_of% pollington_de_mathan) : ∃ m : ℕ → ℕ, (∀ n, 0 < m n) ∧ IsLacunary m ∧ ¬ ∀ ξ : ℝ, Irrational ξ → Dense (Set.range fun n => (↑(ξ * m n) : AddCircle (1 : ℝ))) := h:∀ (m : ℕ → ℕ), (∀ (n : ℕ), 0 < m n) → IsLacunary m → dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m n)))} = 1⊢ ∃ m, (∀ (n : ℕ), 0 < m n) ∧ IsLacunary m ∧ ¬∀ (ξ : ℝ), Irrational ξ → Dense (Set.range fun n => ↑(ξ * ↑(m n))) h:∀ (m : ℕ → ℕ), (∀ (n : ℕ), 0 < m n) → IsLacunary m → dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m n)))} = 1m₀:ℕ → ℕ := fun n => 2 ^ nhm₀:m₀ = fun n => 2 ^ n := rfl⊢ ∃ m, (∀ (n : ℕ), 0 < m n) ∧ IsLacunary m ∧ ¬∀ (ξ : ℝ), Irrational ξ → Dense (Set.range fun n => ↑(ξ * ↑(m n))) have hpos : ∀ n, 0 < m₀ n := h:∀ (m : ℕ → ℕ), (∀ (n : ℕ), 0 < m n) → IsLacunary m → dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m n)))} = 1⊢ ∃ m, (∀ (n : ℕ), 0 < m n) ∧ IsLacunary m ∧ ¬∀ (ξ : ℝ), Irrational ξ → Dense (Set.range fun n => ↑(ξ * ↑(m n))) h:∀ (m : ℕ → ℕ), (∀ (n : ℕ), 0 < m n) → IsLacunary m → dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m n)))} = 1m₀:ℕ → ℕ := fun n => 2 ^ nhm₀:m₀ = fun n => 2 ^ n := rfln:ℕ⊢ 0 < m₀ n; h:∀ (m : ℕ → ℕ), (∀ (n : ℕ), 0 < m n) → IsLacunary m → dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m n)))} = 1m₀:ℕ → ℕ := fun n => 2 ^ nhm₀:m₀ = fun n => 2 ^ n := rfln:ℕ⊢ 0 < (fun n => 2 ^ n) n; All goals completed! 🐙 have hlac : IsLacunary m₀ := h:∀ (m : ℕ → ℕ), (∀ (n : ℕ), 0 < m n) → IsLacunary m → dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m n)))} = 1⊢ ∃ m, (∀ (n : ℕ), 0 < m n) ∧ IsLacunary m ∧ ¬∀ (ξ : ℝ), Irrational ξ → Dense (Set.range fun n => ↑(ξ * ↑(m n))) refine ⟨3 / 2, h:∀ (m : ℕ → ℕ), (∀ (n : ℕ), 0 < m n) → IsLacunary m → dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m n)))} = 1m₀:ℕ → ℕ := fun n => 2 ^ nhm₀:m₀ = fun n => 2 ^ n := rflhpos:∀ (n : ℕ), 0 < m₀ n := fun n => Eq.mpr (id (congrArg (fun _a => 0 < _a n) hm₀)) (pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) n)⊢ 3 / 2 > 1 All goals completed! 🐙, .of_forall fun k => ?_⟩ h:∀ (m : ℕ → ℕ), (∀ (n : ℕ), 0 < m n) → IsLacunary m → dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m n)))} = 1m₀:ℕ → ℕ := fun n => 2 ^ nhm₀:m₀ = fun n => 2 ^ n := rflhpos:∀ (n : ℕ), 0 < m₀ n := fun n => Eq.mpr (id (congrArg (fun _a => 0 < _a n) hm₀)) (pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) n)k:ℕ⊢ 3 / 2 * ↑(2 ^ k) < ↑(2 ^ (k + 1)) h:∀ (m : ℕ → ℕ), (∀ (n : ℕ), 0 < m n) → IsLacunary m → dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m n)))} = 1m₀:ℕ → ℕ := fun n => 2 ^ nhm₀:m₀ = fun n => 2 ^ n := rflhpos:∀ (n : ℕ), 0 < m₀ n := fun n => Eq.mpr (id (congrArg (fun _a => 0 < _a n) hm₀)) (pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) n)k:ℕ⊢ 3 / 2 * 2 ^ k < 2 ^ (k + 1) h:∀ (m : ℕ → ℕ), (∀ (n : ℕ), 0 < m n) → IsLacunary m → dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m n)))} = 1m₀:ℕ → ℕ := fun n => 2 ^ nhm₀:m₀ = fun n => 2 ^ n := rflhpos:∀ (n : ℕ), 0 < m₀ n := fun n => Eq.mpr (id (congrArg (fun _a => 0 < _a n) hm₀)) (pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) n)k:ℕ⊢ 3 / 2 * 2 ^ k < 2 ^ k * 2 nlinarith [pow_pos (show (0 : ℝ) < 2 h:∀ (m : ℕ → ℕ), (∀ (n : ℕ), 0 < m n) → IsLacunary m → dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m n)))} = 1⊢ ∃ m, (∀ (n : ℕ), 0 < m n) ∧ IsLacunary m ∧ ¬∀ (ξ : ℝ), Irrational ξ → Dense (Set.range fun n => ↑(ξ * ↑(m n))) All goals completed! 🐙) k] h:∀ (m : ℕ → ℕ), (∀ (n : ℕ), 0 < m n) → IsLacunary m → dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m n)))} = 1m₀:ℕ → ℕ := fun n => 2 ^ nhm₀:m₀ = fun n => 2 ^ n := rflhpos:∀ (n : ℕ), 0 < m₀ n := fun n => Eq.mpr (id (congrArg (fun _a => 0 < _a n) hm₀)) (pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) n)hlac:IsLacunary m₀ := Exists.intro (3 / 2) ⟨Mathlib.Meta.NormNum.isNNRat_lt_true (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl true), Eventually.of_forall fun k => Eq.mpr (id (congr (congrArg (fun x => LT.lt (3 / 2 * ↑(x k))) hm₀) (congrArg (fun x => ↑(x (k + 1))) hm₀))) (Eq.mpr (id (congr (congrArg (fun x => LT.lt (3 / 2 * x)) (Nat.cast_pow 2 k)) (Nat.cast_pow 2 (k + 1)))) (Eq.mpr (id (congrArg (fun _a => 3 / 2 * 2 ^ k < _a) (pow_succ 2 k))) (lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (k ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 2) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 2) (Eq.refl 4))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 4 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 4 + 0)))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 4))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 4 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 4 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 4 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 3)) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 3 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 3 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 3 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (k ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 3))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 3)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 3 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 3 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3)) (Eq.refl (Int.negOfNat 3)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 4)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (k ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_le_of_neg (Eq.mp (congrArg (fun _a => _a ≤ 0) (CancelDenoms.derive_trans (Eq.trans (congrArg (HSub.hSub (2 ^ k * 2)) (Eq.trans (congrArg (fun x => x * 2 ^ k) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl 3) (Eq.refl 2))) (congrArg (fun x => x * 2 ^ k) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl 3) (Eq.refl 2))))) (congrArg (fun x => 2 ^ k * 2 - x * 2 ^ k) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl 3) (Eq.refl 2)))) (CancelDenoms.sub_subst (CancelDenoms.mul_subst rfl rfl (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (CancelDenoms.mul_subst (CancelDenoms.div_subst rfl (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) rfl (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))))))) (Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le a) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false)))) (Mathlib.Tactic.Linarith.sub_neg_of_lt (pow_pos (have this := Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false); this) k)))))))⟩hd:∀ (ξ : ℝ), Irrational ξ → Dense (Set.range fun n => ↑(ξ * ↑(m₀ n)))⊢ False h:∀ (m : ℕ → ℕ), (∀ (n : ℕ), 0 < m n) → IsLacunary m → dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m n)))} = 1m₀:ℕ → ℕ := fun n => 2 ^ nhm₀:m₀ = fun n => 2 ^ n := rflhpos:∀ (n : ℕ), 0 < m₀ n := fun n => Eq.mpr (id (congrArg (fun _a => 0 < _a n) hm₀)) (pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) n)hlac:IsLacunary m₀ := Exists.intro (3 / 2) ⟨Mathlib.Meta.NormNum.isNNRat_lt_true (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl true), Eventually.of_forall fun k => Eq.mpr (id (congr (congrArg (fun x => LT.lt (3 / 2 * ↑(x k))) hm₀) (congrArg (fun x => ↑(x (k + 1))) hm₀))) (Eq.mpr (id (congr (congrArg (fun x => LT.lt (3 / 2 * x)) (Nat.cast_pow 2 k)) (Nat.cast_pow 2 (k + 1)))) (Eq.mpr (id (congrArg (fun _a => 3 / 2 * 2 ^ k < _a) (pow_succ 2 k))) (lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (k ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 2) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 2) (Eq.refl 4))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 4 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 4 + 0)))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 4))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 4 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 4 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 4 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 3)) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 3 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 3 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 3 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (k ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 3))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 3)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 3 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 3 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3)) (Eq.refl (Int.negOfNat 3)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 4)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (k ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_le_of_neg (Eq.mp (congrArg (fun _a => _a ≤ 0) (CancelDenoms.derive_trans (Eq.trans (congrArg (HSub.hSub (2 ^ k * 2)) (Eq.trans (congrArg (fun x => x * 2 ^ k) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl 3) (Eq.refl 2))) (congrArg (fun x => x * 2 ^ k) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl 3) (Eq.refl 2))))) (congrArg (fun x => 2 ^ k * 2 - x * 2 ^ k) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl 3) (Eq.refl 2)))) (CancelDenoms.sub_subst (CancelDenoms.mul_subst rfl rfl (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (CancelDenoms.mul_subst (CancelDenoms.div_subst rfl (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) rfl (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))))))) (Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le a) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false)))) (Mathlib.Tactic.Linarith.sub_neg_of_lt (pow_pos (have this := Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false); this) k)))))))⟩hd:∀ (ξ : ℝ), Irrational ξ → Dense (Set.range fun n => ↑(ξ * ↑(m₀ n)))hdim:dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m₀ n)))} = 1 := h m₀ hpos hlac⊢ False have hcount : {ξ : ℝ | ¬ Dense (Set.range fun n => (↑(ξ * m₀ n) : AddCircle (1 : ℝ)))}.Countable := Set.Countable.mono (fun ξ hξ => h:∀ (m : ℕ → ℕ), (∀ (n : ℕ), 0 < m n) → IsLacunary m → dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m n)))} = 1m₀:ℕ → ℕ := fun n => 2 ^ nhm₀:m₀ = fun n => 2 ^ n := rflhpos:∀ (n : ℕ), 0 < m₀ n := fun n => Eq.mpr (id (congrArg (fun _a => 0 < _a n) hm₀)) (pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) n)hlac:IsLacunary m₀ := Exists.intro (3 / 2) ⟨Mathlib.Meta.NormNum.isNNRat_lt_true (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl true), Eventually.of_forall fun k => Eq.mpr (id (congr (congrArg (fun x => LT.lt (3 / 2 * ↑(x k))) hm₀) (congrArg (fun x => ↑(x (k + 1))) hm₀))) (Eq.mpr (id (congr (congrArg (fun x => LT.lt (3 / 2 * x)) (Nat.cast_pow 2 k)) (Nat.cast_pow 2 (k + 1)))) (Eq.mpr (id (congrArg (fun _a => 3 / 2 * 2 ^ k < _a) (pow_succ 2 k))) (lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (k ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 2) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 2) (Eq.refl 4))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 4 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 4 + 0)))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 4))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 4 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 4 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 4 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 3)) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 3 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 3 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 3 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (k ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 3))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 3)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 3 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 3 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3)) (Eq.refl (Int.negOfNat 3)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 4)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (k ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_le_of_neg (Eq.mp (congrArg (fun _a => _a ≤ 0) (CancelDenoms.derive_trans (Eq.trans (congrArg (HSub.hSub (2 ^ k * 2)) (Eq.trans (congrArg (fun x => x * 2 ^ k) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl 3) (Eq.refl 2))) (congrArg (fun x => x * 2 ^ k) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl 3) (Eq.refl 2))))) (congrArg (fun x => 2 ^ k * 2 - x * 2 ^ k) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl 3) (Eq.refl 2)))) (CancelDenoms.sub_subst (CancelDenoms.mul_subst rfl rfl (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (CancelDenoms.mul_subst (CancelDenoms.div_subst rfl (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) rfl (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))))))) (Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le a) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false)))) (Mathlib.Tactic.Linarith.sub_neg_of_lt (pow_pos (have this := Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false); this) k)))))))⟩hd:∀ (ξ : ℝ), Irrational ξ → Dense (Set.range fun n => ↑(ξ * ↑(m₀ n)))hdim:dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m₀ n)))} = 1 := h m₀ hpos hlacξ:ℝhξ:ξ ∈ {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m₀ n)))}⊢ ξ ∈ Set.range ?m.146 h:∀ (m : ℕ → ℕ), (∀ (n : ℕ), 0 < m n) → IsLacunary m → dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m n)))} = 1m₀:ℕ → ℕ := fun n => 2 ^ nhm₀:m₀ = fun n => 2 ^ n := rflhpos:∀ (n : ℕ), 0 < m₀ n := fun n => Eq.mpr (id (congrArg (fun _a => 0 < _a n) hm₀)) (pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) n)hlac:IsLacunary m₀ := Exists.intro (3 / 2) ⟨Mathlib.Meta.NormNum.isNNRat_lt_true (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl true), Eventually.of_forall fun k => Eq.mpr (id (congr (congrArg (fun x => LT.lt (3 / 2 * ↑(x k))) hm₀) (congrArg (fun x => ↑(x (k + 1))) hm₀))) (Eq.mpr (id (congr (congrArg (fun x => LT.lt (3 / 2 * x)) (Nat.cast_pow 2 k)) (Nat.cast_pow 2 (k + 1)))) (Eq.mpr (id (congrArg (fun _a => 3 / 2 * 2 ^ k < _a) (pow_succ 2 k))) (lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (k ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 2) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 2) (Eq.refl 4))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 4 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 4 + 0)))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 4))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 4 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 4 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 4 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 3)) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 3 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 3 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 3 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (k ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 3))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 3)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 3 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 3 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3)) (Eq.refl (Int.negOfNat 3)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 4)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (k ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_le_of_neg (Eq.mp (congrArg (fun _a => _a ≤ 0) (CancelDenoms.derive_trans (Eq.trans (congrArg (HSub.hSub (2 ^ k * 2)) (Eq.trans (congrArg (fun x => x * 2 ^ k) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl 3) (Eq.refl 2))) (congrArg (fun x => x * 2 ^ k) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl 3) (Eq.refl 2))))) (congrArg (fun x => 2 ^ k * 2 - x * 2 ^ k) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl 3) (Eq.refl 2)))) (CancelDenoms.sub_subst (CancelDenoms.mul_subst rfl rfl (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (CancelDenoms.mul_subst (CancelDenoms.div_subst rfl (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) rfl (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))))))) (Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le a) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false)))) (Mathlib.Tactic.Linarith.sub_neg_of_lt (pow_pos (have this := Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false); this) k)))))))⟩hd:∀ (ξ : ℝ), Irrational ξ → Dense (Set.range fun n => ↑(ξ * ↑(m₀ n)))hdim:dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m₀ n)))} = 1 := h m₀ hpos hlacξ:ℝhξ:ξ ∈ {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m₀ n)))}hξr:ξ ∉ Set.range ?m.146⊢ False; All goals completed! 🐙) (Set.countable_range _) h:∀ (m : ℕ → ℕ), (∀ (n : ℕ), 0 < m n) → IsLacunary m → dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m n)))} = 1m₀:ℕ → ℕ := fun n => 2 ^ nhm₀:m₀ = fun n => 2 ^ n := rflhpos:∀ (n : ℕ), 0 < m₀ n := fun n => Eq.mpr (id (congrArg (fun _a => 0 < _a n) hm₀)) (pow_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2))) n)hlac:IsLacunary m₀ := Exists.intro (3 / 2) ⟨Mathlib.Meta.NormNum.isNNRat_lt_true (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl true), Eventually.of_forall fun k => Eq.mpr (id (congr (congrArg (fun x => LT.lt (3 / 2 * ↑(x k))) hm₀) (congrArg (fun x => ↑(x (k + 1))) hm₀))) (Eq.mpr (id (congr (congrArg (fun x => LT.lt (3 / 2 * x)) (Nat.cast_pow 2 k)) (Nat.cast_pow 2 (k + 1)))) (Eq.mpr (id (congrArg (fun _a => 3 / 2 * 2 ^ k < _a) (pow_succ 2 k))) (lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (k ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 2) (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 2) (Eq.refl 4))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 4 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 4 + 0)))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 4))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 4 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 4 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 4 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 3)) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 3 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 3 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 3 + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (k ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Nat.rawCast 3))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 3)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 3 + 0))) (Mathlib.Tactic.Ring.zero_mul ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 3 + 0)))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 3)) (Eq.refl (Int.negOfNat 3)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Tactic.Ring.add_overlap_pf (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 4)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 3)) (Eq.refl (Int.ofNat 1)))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)) (Mathlib.Tactic.Ring.pow_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Tactic.Ring.atom_pf k) (Mathlib.Tactic.Ring.pow_add (Mathlib.Tactic.Ring.single_pow (Mathlib.Tactic.Ring.pow_prod_atom (Nat.rawCast 2) (k ^ Nat.rawCast 1 * Nat.rawCast 1))) (Mathlib.Tactic.Ring.pow_zero (Nat.rawCast 2 + 0)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))) (Mathlib.Tactic.Ring.mul_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))) (Mathlib.Tactic.Ring.zero_mul (Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_zero_add ((Nat.rawCast 2 + 0) ^ (k ^ Nat.rawCast 1 * Nat.rawCast 1) * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero (Nat.rawCast 2 + 0) (k ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero)))) (Mathlib.Tactic.Linarith.add_lt_of_le_of_neg (Eq.mp (congrArg (fun _a => _a ≤ 0) (CancelDenoms.derive_trans (Eq.trans (congrArg (HSub.hSub (2 ^ k * 2)) (Eq.trans (congrArg (fun x => x * 2 ^ k) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl 3) (Eq.refl 2))) (congrArg (fun x => x * 2 ^ k) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl 3) (Eq.refl 2))))) (congrArg (fun x => 2 ^ k * 2 - x * 2 ^ k) (Mathlib.Meta.NormNum.IsNNRat.to_eq (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 3))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 3 1)) (Eq.refl 2))) (Eq.refl 3) (Eq.refl 2)))) (CancelDenoms.sub_subst (CancelDenoms.mul_subst rfl rfl (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (CancelDenoms.mul_subst (CancelDenoms.div_subst rfl (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_div (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.IsNNRat.to_isNat (Mathlib.Meta.NormNum.isNNRat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))) (Mathlib.Meta.NormNum.isNNRat_inv_pos (Mathlib.Meta.NormNum.IsNat.to_isNNRat (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) (Eq.refl (Nat.mul 2 1)) (Eq.refl 2)))))) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)))) rfl (Mathlib.Meta.NormNum.isNat_eq_true (Mathlib.Meta.NormNum.isNat_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl 2)) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2))))))) (Mathlib.Tactic.Linarith.mul_nonpos (Mathlib.Tactic.Linarith.sub_nonpos_of_le a) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false)))) (Mathlib.Tactic.Linarith.sub_neg_of_lt (pow_pos (have this := Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_zero) (Mathlib.Meta.NormNum.isNat_ofNat ℝ (Eq.refl 2)) (Eq.refl false); this) k)))))))⟩hd:∀ (ξ : ℝ), Irrational ξ → Dense (Set.range fun n => ↑(ξ * ↑(m₀ n)))hdim:0 = 1hcount:{ξ | ¬Dense (Set.range fun n => ↑(ξ * ↑(m₀ n)))}.Countable⊢ False All goals completed! 🐙

Furstenberg's theorem [Fur67] (the $\times 2, \times 3$ case). For every irrational number $\xi$, the two-parameter family $({\xi , 2^m 3^n})_{m, n \ge 1}$ is dense modulo one.

@[category research solved, AMS 11] theorem declaration uses 'sorry'furstenberg_two_three (ξ : ℝ) (hξ : Irrational ξ) : Dense {x : AddCircle (1 : ℝ) | ∃ m n : ℕ, 0 < m ∧ 0 < n ∧ x = ↑(ξ * (2 ^ m * 3 ^ n : ℕ))} := ξ:ℝhξ:Irrational ξ⊢ Dense {x | ∃ m n, 0 < m ∧ 0 < n ∧ x = ↑(ξ * ↑(2 ^ m * 3 ^ n))} All goals completed! 🐙

Boshernitzan's theorem [Bos94]. Given a real sublacunary sequence $r$, the set of real numbers $\xi$ for which $({\xi r_n})_{n \ge 1}$ is not dense modulo one has Hausdorff dimension zero.

@[category research solved, AMS 11] theorem declaration uses 'sorry'boshernitzan (r : ℕ → ℝ) (hr : ∀ n, 0 < r n) (hunb : ¬ BddAbove (Set.range r)) (hsub : Tendsto (fun n => r (n + 1) / r n) atTop (nhds 1)) : dimH {ξ : ℝ | ¬ Dense (Set.range fun n => (↑(ξ * r n) : AddCircle (1 : ℝ)))} = 0 := r:ℕ → ℝhr:∀ (n : ℕ), 0 < r nhunb:¬BddAbove (Set.range r)hsub:Tendsto (fun n => r (n + 1) / r n) atTop (nhds 1)⊢ dimH {ξ | ¬Dense (Set.range fun n => ↑(ξ * r n))} = 0 All goals completed! 🐙

The sequence defined by $m_0 = 2$ and $m_{n+1} = \lceil m_n (1 + 1/\log n) \rceil$.

noncomputable def mSeq : ℕ → ℕ | 0 => 2 | (n + 1) => ⌈(mSeq n : ℝ) * (1 + 1 / Real.log n)⌉₊

The sequence $m$ eventually grows at least geometrically with a logarithmic correction.

def IsGenuinelySublacunary (m : ℕ → ℕ) : Prop := ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, (1 + c / Real.log n) ≤ (m (n+1) : ℝ) / m n

The sequence mSeq, given by $m_{n+1} = \lceil m_n (1 + 1/\log n) \rceil$, is genuinely sublacunary: taking $c = 1$, we have $m_{n+1}/m_n \ge 1 + 1/\log n$ because $\lceil m_n (1 + 1/\log n) \rceil \ge m_n (1 + 1/\log n)$.

@[category test, AMS 11] lemma example_isGenuineSublacunary : IsGenuinelySublacunary mSeq := ⊢ IsGenuinelySublacunary mSeq -- Every term of `mSeq` is positive. have mSeq_pos : ∀ n, 0 < mSeq n := ⊢ IsGenuinelySublacunary mSeq n:ℕ⊢ 0 < mSeq n induction n with ⊢ 0 < mSeq 0 All goals completed! 🐙 k:ℕih:0 < mSeq k⊢ 0 < mSeq (k + 1) k:ℕih:0 < mSeq k⊢ 0 < ↑(mSeq k) * (1 + 1 / Real.log ↑k) exact mul_pos (k:ℕih:0 < mSeq k⊢ 0 < ↑(mSeq k) All goals completed! 🐙) (k:ℕih:0 < mSeq k⊢ 0 < 1 + 1 / Real.log ↑k All goals completed! 🐙) mSeq_pos:∀ (n : ℕ), 0 < mSeq n := fun n => Nat.recAux (of_eq_true Nat.ofNat_pos._simp_1) (fun k ih => Eq.mpr (id example_isGenuineSublacunary._simp_4) (mul_pos (cast (Eq.symm (Eq.trans (congrArg (fun x => x < ↑(mSeq k)) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1)) ih) (add_pos_of_pos_of_nonneg (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl (Nat.ble 1 1))) (Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl (Nat.ble 1 1))) (Real.log_natCast_nonneg k))))) nn:ℕ⊢ 1 + 1 / Real.log ↑n ≤ ↑(mSeq (n + 1)) / ↑(mSeq n) have hpos : (0 : ℝ) < (mSeq n : ℝ) := ⊢ IsGenuinelySublacunary mSeq All goals completed! 🐙 mSeq_pos:∀ (n : ℕ), 0 < mSeq n := fun n => Nat.recAux (of_eq_true Nat.ofNat_pos._simp_1) (fun k ih => Eq.mpr (id example_isGenuineSublacunary._simp_4) (mul_pos (cast (Eq.symm (Eq.trans (congrArg (fun x => x < ↑(mSeq k)) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1)) ih) (add_pos_of_pos_of_nonneg (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl (Nat.ble 1 1))) (Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl (Nat.ble 1 1))) (Real.log_natCast_nonneg k))))) nn:ℕhpos:0 < ↑(mSeq n) := cast (Eq.symm (Eq.trans (congrArg (fun x => x < ↑(mSeq n)) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1)) (mSeq_pos n)⊢ (1 + 1 / Real.log ↑n) * ↑(mSeq n) ≤ ↑(mSeq (n + 1)) mSeq_pos:∀ (n : ℕ), 0 < mSeq n := fun n => Nat.recAux (of_eq_true Nat.ofNat_pos._simp_1) (fun k ih => Eq.mpr (id example_isGenuineSublacunary._simp_4) (mul_pos (cast (Eq.symm (Eq.trans (congrArg (fun x => x < ↑(mSeq k)) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1)) ih) (add_pos_of_pos_of_nonneg (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl (Nat.ble 1 1))) (Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl (Nat.ble 1 1))) (Real.log_natCast_nonneg k))))) nn:ℕhpos:0 < ↑(mSeq n) := cast (Eq.symm (Eq.trans (congrArg (fun x => x < ↑(mSeq n)) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1)) (mSeq_pos n)⊢ (1 + 1 / Real.log ↑n) * ↑(mSeq n) ≤ ↑⌈↑(mSeq n) * (1 + 1 / Real.log ↑n)⌉₊ mSeq_pos:∀ (n : ℕ), 0 < mSeq n := fun n => Nat.recAux (of_eq_true Nat.ofNat_pos._simp_1) (fun k ih => Eq.mpr (id example_isGenuineSublacunary._simp_4) (mul_pos (cast (Eq.symm (Eq.trans (congrArg (fun x => x < ↑(mSeq k)) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1)) ih) (add_pos_of_pos_of_nonneg (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl (Nat.ble 1 1))) (Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one) (Eq.refl (Nat.ble 1 1))) (Real.log_natCast_nonneg k))))) nn:ℕhpos:0 < ↑(mSeq n) := cast (Eq.symm (Eq.trans (congrArg (fun x => x < ↑(mSeq n)) (Eq.symm Nat.cast_zero)) Nat.cast_lt._simp_1)) (mSeq_pos n)⊢ ↑(mSeq n) * (1 + 1 / Real.log ↑n) ≤ ↑⌈↑(mSeq n) * (1 + 1 / Real.log ↑n)⌉₊ All goals completed! 🐙

The sequence $m$ eventually grows at least as fast as $\exp(n^{\alpha})$, i.e., super-exponential growth when $\alpha > 1$, and stretched-exponential when $0 < \alpha < 1$.

def HasIntermediateGrowth (α : ℝ) (m : ℕ → ℕ) : Prop := ∀ᶠ (n : ℕ) in atTop, Real.exp ((n : ℝ) ^ α) ≤ m n

mSeq has intermediate (subexponential but super-polynomial) growth: for every 0 < α < 1 its terms eventually dominate $\exp(n^\alpha)$.

@[category test, AMS 11] lemma declaration uses 'sorry'example_hasIntermediateGrowth (α : ℝ) (hα₀ : 0 < α) (hα₁ : α < 1) : HasIntermediateGrowth α mSeq := α:ℝhα₀:0 < αhα₁:α < 1⊢ HasIntermediateGrowth α mSeq All goals completed! 🐙

Problem 10.6. Find a very rapidly increasing sequence $(m_n){n \ge 1}$ of positive integers such that $({\xi m_n}){n \ge 1}$ is dense modulo one for every irrational number $\xi$. Note: Furstenberg's $2^m3^n$ is sublacunary but requires two parameters.

@[category research open, AMS 11] theorem declaration uses 'sorry'problem_10_6_variant_1 : ∃ m : ℕ → ℕ, StrictMono m ∧ IsGenuinelySublacunary m ∧ ∀ ξ : ℝ, Irrational ξ → Dense (Set.range fun n => (↑(ξ * m n) : AddCircle (1 : ℝ))) := ⊢ ∃ m, StrictMono m ∧ IsGenuinelySublacunary m ∧ ∀ (ξ : ℝ), Irrational ξ → Dense (Set.range fun n => ↑(ξ * ↑(m n))) All goals completed! 🐙

Problem 10.6, intermediate-growth variant.

@[category research open, AMS 11] theorem declaration uses 'sorry'problem_10_6_variant_2 : ∃ m : ℕ → ℕ, StrictMono m ∧ (∃ α : ℝ, 0 < α ∧ α < 1 ∧ HasIntermediateGrowth α m) ∧ ∀ ξ : ℝ, Irrational ξ → Dense (Set.range fun n => (↑(ξ * m n) : AddCircle (1 : ℝ))) := ⊢ ∃ m, StrictMono m ∧ (∃ α, 0 < α ∧ α < 1 ∧ HasIntermediateGrowth α m) ∧ ∀ (ξ : ℝ), Irrational ξ → Dense (Set.range fun n => ↑(ξ * ↑(m n))) All goals completed! 🐙 end Bugeaud06