goodτ

Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace

URI: https://scilib.ai/kg/mathlib#Besicovitch.goodτ

← MathLib Explorer

English

One has 1 < goodτ(E), i.e., the Besicovitch τ parameter is strictly greater than 1.

Русский

Из одного следует, что goodτ(E) > 1.

LaTeX

$$$$1 < goodτ(E)$$$$

Lean4

/-- A number `τ > 1`, but chosen close enough to `1` so that the construction in the Besicovitch
covering theorem using this parameter `τ` will give the smallest possible number of covering
families. -/
def goodτ : ℝ :=
  1 + goodδ E / 4

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru