Other results

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

TheoremLebesgue's density theorem#

At almost every point a null-measurable set has density one or zero, according to whether the point lies in the set.

TauCeti.ae_hasDensityAt_indicator.{u_1} {α : Type u_1} [MetricSpace α] [MeasurableSpace α]
  [SecondCountableTopology α] [BorelSpace α] [HasBesicovitchCovering α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {s : Set α}
  (hs : MeasureTheory.NullMeasurableSet s μ) :
  ∀ᵐ (x : α) ∂μ, TauCeti.HasDensityAt μ s x (s.indicator 1 x)
Lean

Formalized in Tau Ceti as TauCeti.ae_hasDensityAt_indicator.

Other forms

Lebesgue's density theorem for a null-measurable set s. Formalized in Tau Ceti as MeasureTheory.NullMeasurableSet.ae_tendsto_measure_inter_div.

MeasureTheory.NullMeasurableSet.ae_tendsto_measure_inter_div.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} [MetricSpace α]
  [SecondCountableTopology α] [BorelSpace α] [HasBesicovitchCovering α]
  [MeasureTheory.IsLocallyFiniteMeasure μ] (hs : MeasureTheory.NullMeasurableSet s μ) :
  ∀ᵐ (x : α) ∂μ,
    Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r))
      (nhdsWithin 0 (Set.Ioi 0)) (nhds (s.indicator 1 x))

Lebesgue's density theorem. Formalized in Tau Ceti as TauCeti.essentialExterior_ae_eq.

TauCeti.essentialExterior_ae_eq.{u_1} {α : Type u_1} [MetricSpace α] [MeasurableSpace α]
  [SecondCountableTopology α] [BorelSpace α] [HasBesicovitchCovering α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {s : Set α}
  (hs : MeasureTheory.NullMeasurableSet s μ) : TauCeti.essentialExterior μ s =ᵐ[μ] sᶜ

Lebesgue's density theorem. Formalized in Tau Ceti as TauCeti.essentialInterior_ae_eq.

TauCeti.essentialInterior_ae_eq.{u_1} {α : Type u_1} [MetricSpace α] [MeasurableSpace α]
  [SecondCountableTopology α] [BorelSpace α] [HasBesicovitchCovering α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {s : Set α}
  (hs : MeasureTheory.NullMeasurableSet s μ) : TauCeti.essentialInterior μ s =ᵐ[μ] s

Lebesgue's density theorem. Formalized in Tau Ceti as TauCeti.measure_essentialBoundary.

TauCeti.measure_essentialBoundary.{u_1} {α : Type u_1} [MetricSpace α] [MeasurableSpace α]
  [SecondCountableTopology α] [BorelSpace α] [HasBesicovitchCovering α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure μ] {s : Set α}
  (hs : MeasureTheory.NullMeasurableSet s μ) : μ (TauCeti.essentialBoundary μ s) = 0
Sources
LeanTauCeti.ae_hasDensityAt_indicator · MeasureTheory.NullMeasurableSet.ae_tendsto_measure_inter_div · TauCeti.essentialExterior_ae_eq · TauCeti.essentialInterior_ae_eq · TauCeti.measure_essentialBoundary

TheoremLebesgue's differentiation theorem#

Lebesgue's differentiation theorem for a locally finite measure in a space with the Besicovitch covering property: for a locally integrable function f, at almost every point x the averages of f over the closed balls around x tend to f x.

Besicovitch.ae_tendsto_average_closedBall.{u_1, u_2} {β : Type u_1} {F : Type u_2} [MetricSpace β]
  [MeasurableSpace β] [BorelSpace β] [SecondCountableTopology β] [HasBesicovitchCovering β]
  [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (μ : MeasureTheory.Measure β)
  [MeasureTheory.IsLocallyFiniteMeasure μ] {f : β → F} (hf : MeasureTheory.LocallyIntegrable f μ) :
  ∀ᵐ (x : β) ∂μ,
    Filter.Tendsto (fun r => ⨍ (y : β) in Metric.closedBall x r, f y ∂μ) (nhdsWithin 0 (Set.Ioi 0))
      (nhds (f x))
Lean

Formalized in Tau Ceti as Besicovitch.ae_tendsto_average_closedBall.

Other forms

Lebesgue differentiation theorem along concentric closed balls. Formalized in Tau Ceti as IsUnifLocDoublingMeasure.ae_tendsto_average_closedBall_norm_sub.

IsUnifLocDoublingMeasure.ae_tendsto_average_closedBall_norm_sub.{u_1, u_2} {α : Type u_1}
  {E : Type u_2} [PseudoMetricSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [IsUnifLocDoublingMeasure μ] [SecondCountableTopology α] [BorelSpace α]
  [MeasureTheory.IsLocallyFiniteMeasure μ] [NormedAddCommGroup E] {f : α → E}
  (hf : MeasureTheory.LocallyIntegrable f μ) :
  ∀ᵐ (x : α) ∂μ,
    Filter.Tendsto (fun r => ⨍ (y : α) in Metric.closedBall x r, ‖f y - f x‖ ∂μ)
      (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
Sources
LeanBesicovitch.ae_tendsto_average_closedBall · IsUnifLocDoublingMeasure.ae_tendsto_average_closedBall_norm_sub
Used by 2
Used byThe Gauss–Green formula, Dχ_s = -ν_s |Dχ_s| · The isoperimetric inequality on the line

TheoremMinkowski's convex body theorem for the integer lattice#

A compact convex set s ⊆ η → ℝ, symmetric about the origin, of volume at least 2 ^ |η| contains a nonzero integer vector.

MeasureTheory.exists_ne_zero_int_vec_mem_of_two_pow_le_volume.{u_1} {η : Type u_1} [Fintype η]
  [Nonempty η] {s : Set (η → ℝ)} (h_symm : ∀ x ∈ s, -x ∈ s) (h_conv : Convex ℝ s)
  (h_cpt : IsCompact s) (h : 2 ^ Fintype.card η ≤ MeasureTheory.volume s) :
  ∃ z, z ≠ 0 ∧ (fun k => ↑(z k)) ∈ s
Lean

Formalized in Tau Ceti as MeasureTheory.exists_ne_zero_int_vec_mem_of_two_pow_le_volume.

Sources
LeanMeasureTheory.exists_ne_zero_int_vec_mem_of_two_pow_le_volume
Used by 2
Used byDirichlet's theorem, nearest-integer form · Minkowski's linear forms theorem

TheoremScalar Radon–Nikodym theorem#

If the variation of a scalar measure is absolutely continuous with respect to a sigma-finite measure, its scalar density reconstructs it.

MeasureTheory.VectorMeasure.withDensityᵥ_scalarRNDeriv.{u_1, u_2} {X : Type u_1} {𝕜 : Type u_2}
  [MeasurableSpace X] [RCLike 𝕜] (μ : MeasureTheory.VectorMeasure X 𝕜) (ν : MeasureTheory.Measure X)
  [MeasureTheory.SigmaFinite ν] (hμν : μ.variation.AbsolutelyContinuous ν) :
  ν.withDensityᵥ (μ.scalarRNDeriv ν) = μ
Lean

Formalized in Tau Ceti as MeasureTheory.VectorMeasure.withDensityᵥ_scalarRNDeriv.

Sources
LeanMeasureTheory.VectorMeasure.withDensityᵥ_scalarRNDeriv

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.