Constructions

Results named in Tau Ceti's TauCeti.MeasureTheory.Constructions modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe Borel graph theorem#

A map between standard Borel spaces is measurable if and only if its graph is measurable.

TauCeti.measurableSet_graph_iff_measurable.{u_1, u_2} {X : Type u_1} {Y : Type u_2}
  [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y]
  {f : X → Y} : MeasurableSet (Function.graph f) ↔ Measurable f

Lean

Formalized in Tau Ceti as TauCeti.measurableSet_graph_iff_measurable.

Other forms

The Borel graph theorem for partial maps. Formalized in Tau Ceti as TauCeti.measurableSet_graphOn_iff.

TauCeti.measurableSet_graphOn_iff.{u_1, u_2} {X : Type u_1} {Y : Type u_2} [MeasurableSpace X]
  [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y] {s : Set X} {f : X → Y} :
  MeasurableSet (Set.graphOn f s) ↔ MeasurableSet s ∧ Measurable (s.domRestrict f)

The Borel graph theorem, analytic form. Formalized in Tau Ceti as TauCeti.analyticSet_graph_iff_measurable.

TauCeti.analyticSet_graph_iff_measurable.{u_1, u_2} {X : Type u_1} {Y : Type u_2}
  [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y]
  [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] {f : X → Y} :
  MeasureTheory.AnalyticSet (Function.graph f) ↔ Measurable f

Sources

• Tau Ceti documentation: TauCeti.measurableSet_graph_iff_measurable
• Source of TauCeti.measurableSet_graph_iff_measurable in TauCeti/MeasureTheory/Constructions/Polish/Graph.lean

LeanTauCeti.measurableSet_graph_iff_measurable · TauCeti.measurableSet_graphOn_iff · TauCeti.analyticSet_graph_iff_measurable

Uses 2

Proof usesLusin–Souslin for vertical sections · Souslin's theorem for graphs

TheoremLusin–Souslin for vertical sections#

If a measurable subset G of a product of standard Borel spaces has at most one point above each x, its projection G → X is a measurable embedding.

MeasurableSet.measurableEmbedding_domRestrict_fst.{u_1, u_2} {X : Type u_1} {Y : Type u_2}
  [MeasurableSpace X] [StandardBorelSpace X] [MeasurableSpace Y] [StandardBorelSpace Y]
  {G : Set (X × Y)} (hG : MeasurableSet G) (hinj : Set.InjOn Prod.fst G) :
  MeasurableEmbedding (G.domRestrict Prod.fst)

Lean

Formalized in Tau Ceti as MeasurableSet.measurableEmbedding_domRestrict_fst.

Sources

• Tau Ceti documentation: MeasurableSet.measurableEmbedding_domRestrict_fst
• Source of MeasurableSet.measurableEmbedding_domRestrict_fst in TauCeti/MeasureTheory/Constructions/Polish/Graph.lean

LeanMeasurableSet.measurableEmbedding_domRestrict_fst

Used by 1

Used byThe Borel graph theorem

TheoremThe perfect set theorem for Borel sets (Alexandrov–Hausdorff)#

An uncountable Borel subset of a Polish space contains the range of a continuous injection of Cantor space.

MeasurableSet.exists_nat_bool_injection_of_not_countable.{u} {X : Type u} [TopologicalSpace X]
  [PolishSpace X] [MeasurableSpace X] [BorelSpace X] {s : Set X} (hs : MeasurableSet s)
  (hunc : ¬s.Countable) : ∃ f, Set.range f ⊆ s ∧ Continuous f ∧ Function.Injective f

Lean

Formalized in Tau Ceti as MeasurableSet.exists_nat_bool_injection_of_not_countable.

Sources

• Tau Ceti documentation: MeasurableSet.exists_nat_bool_injection_of_not_countable
• Source of MeasurableSet.exists_nat_bool_injection_of_not_countable in TauCeti/MeasureTheory/Constructions/Polish/Perfect.lean

LeanMeasurableSet.exists_nat_bool_injection_of_not_countable

Used by 1

Used bySilver's theorem relative to a Borel subset

TheoremRadial fundamental theorem of calculus#

For a C¹ function f with compact support on a nontrivial finite-dimensional real normed space of dimension d, ∫ ‖x‖ ^ (-d) * f' x x ∂μ = -(d * μ (ball 0 1)) * f 0.

In the language of distributions, div (x / ‖x‖ ^ d) = d μ(ball 0 1) δ₀.

TauCeti.integral_norm_rpow_neg_finrank_mul_fderiv_apply_self.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E]
  [BorelSpace E] [Nontrivial E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {f : E → ℝ}
  (hf : ContDiff ℝ 1 f) (hc : HasCompactSupport f) :
  ∫ (x : E), ‖x‖ ^ (-↑(Module.finrank ℝ E)) * (fderiv ℝ f x) x ∂μ =
    -(↑(Module.finrank ℝ E) * μ.real (Metric.ball 0 1)) * f 0

Lean

Formalized in Tau Ceti as TauCeti.integral_norm_rpow_neg_finrank_mul_fderiv_apply_self.

Sources

• Tau Ceti documentation: TauCeti.integral_norm_rpow_neg_finrank_mul_fderiv_apply_self
• Source of TauCeti.integral_norm_rpow_neg_finrank_mul_fderiv_apply_self in TauCeti/MeasureTheory/Constructions/HaarToSphere.lean

LeanTauCeti.integral_norm_rpow_neg_finrank_mul_fderiv_apply_self

Used by 1

Used byThe Calderón–Zygmund estimate ‖D²u‖_p ≤ C ‖Δu‖_p

TheoremSouslin's theorem for graphs#

A map from a Hausdorff space with its Borel sets measurable to a Polish space, whose graph is analytic, is measurable.

MeasureTheory.AnalyticSet.measurable_of_graph.{u_1, u_2} {X : Type u_1} {Y : Type u_2}
  [TopologicalSpace X] [T2Space X] [MeasurableSpace X] [OpensMeasurableSpace X] [TopologicalSpace Y]
  [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y] {f : X → Y}
  (hf : MeasureTheory.AnalyticSet (Function.graph f)) : Measurable f

Lean

Formalized in Tau Ceti as MeasureTheory.AnalyticSet.measurable_of_graph.

Sources

• Tau Ceti documentation: MeasureTheory.AnalyticSet.measurable_of_graph
• Source of MeasureTheory.AnalyticSet.measurable_of_graph in TauCeti/MeasureTheory/Constructions/Polish/Graph.lean

LeanMeasureTheory.AnalyticSet.measurable_of_graph

Used by 1

Used byThe Borel graph theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.