exists_norm_nsmul_le — Mathlib

English

A general Dirichlet-type result for AddCircle: for ξ ∈ A, if certain mass-condition holds, there exists j in a short interval with ∥j·ξ∥ ≤ δ.

Русский

Обобщённый результат Дирихле для AddCircle: для ξ ∈ A, при условии массы существует j в коротком интервале, такое что ∥j·ξ∥ ≤ δ.

LaTeX

$$$$ \\exists j \\in [1,n], \\; \\|j\\cdot \\xi\\| \\le \\delta. $$$$

Lean4

/-- A general version of **Dirichlet's approximation theorem**.

See also `AddCircle.exists_norm_nsmul_le`. -/
theorem _root_.NormedAddCommGroup.exists_norm_nsmul_le {A : Type*} [NormedAddCommGroup A] [CompactSpace A]
    [PreconnectedSpace A] [MeasurableSpace A] [BorelSpace A] {μ : Measure A} [μ.IsAddHaarMeasure] (ξ : A) {n : ℕ}
    (hn : 0 < n) (δ : ℝ) (hδ : μ univ ≤ (n + 1) • μ (closedBall (0 : A) (δ / 2))) : ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ :=
  by
  have : IsFiniteMeasure μ := CompactSpace.isFiniteMeasure
  let B : Icc 0 n → Set A := fun j ↦ closedBall ((j : ℕ) • ξ) (δ / 2)
  have hB : ∀ j, IsClosed (B j) := fun j ↦ isClosed_closedBall
  suffices ¬Pairwise (Disjoint on B)
    by
    obtain ⟨i, j, hij, x, hx⟩ := exists_lt_mem_inter_of_not_pairwise_disjoint this
    refine ⟨j - i, ⟨le_tsub_of_add_le_left hij, ?_⟩, ?_⟩
    · simpa only [tsub_le_iff_right] using j.property.2.trans le_self_add
    · rw [sub_nsmul _ (Subtype.coe_le_coe.mpr hij.le), ← sub_eq_add_neg, ← dist_eq_norm]
      exact
        (dist_triangle ((j : ℕ) • ξ) x ((i : ℕ) • ξ)).trans
          (by linarith [mem_closedBall.mp hx.1, mem_closedBall'.mp hx.2])
  by_contra h
  apply hn.ne'
  have h' : ⋃ j, B j = univ :=
    by
    rw [← (isClosed_iUnion_of_finite hB).measure_eq_univ_iff_eq (μ := μ)]
    refine le_antisymm (μ.mono (subset_univ _)) ?_
    simp_rw [measure_iUnion h (fun _ ↦ measurableSet_closedBall), tsum_fintype, B, μ.addHaar_closedBall_center,
      Finset.sum_const, Finset.card_univ, Fintype.card_Icc, Nat.card_Icc, tsub_zero]
    exact hδ
  replace hδ : 0 ≤ δ / 2 := by
    by_contra contra
    suffices μ (closedBall 0 (δ / 2)) = 0
      by
      apply isOpen_univ.measure_ne_zero μ univ_nonempty <| le_zero_iff.mp <| le_trans hδ _
      simp [this]
    rw [not_le, ← closedBall_eq_empty (x := (0 : A))] at contra
    simp [contra]
  have h'' : ∀ j, (B j).Nonempty := by intro j; rwa [nonempty_closedBall]
  simpa using subsingleton_of_disjoint_isClosed_iUnion_eq_univ h'' h hB h'

Похожие утверждения