class MeasureTheory.Measure.IsDoubling {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (μ : MeasureTheory.Measure X) (A : outParam NNReal) : Prop

A doubling measure is a measure on a metric space with the condition that doubling the radius of a ball only increases the volume by a constant factor, independent of the ball.

• measure_ball_two_le_same : ∀ (x : X) (r : ℝ), μ (Metric.ball x (2 * r)) ≤ ↑A * μ (Metric.ball x r)

theorem MeasureTheory.ball_subset_ball_of_le {X : Type u_1} [PseudoMetricSpace X] {x x' : X} {r r' : ℝ} (hr : dist x x' + r' ≤ r) : Metric.ball x' r' ⊆ Metric.ball x r

theorem MeasureTheory.IsDoubling.mono {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] {A' : NNReal} (h : A ≤ A') : μ.IsDoubling A'

theorem MeasureTheory.measure_real_ball_two_le_same {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] (x : X) (r : ℝ) : μ.real (Metric.ball x (2 * r)) ≤ ↑A * μ.real (Metric.ball x r)

theorem MeasureTheory.measure_real_ball_pos {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.IsOpenPosMeasure] (x : X) {r : ℝ} (hr : 0 < r) : 0 < μ.real (Metric.ball x r)

theorem MeasureTheory.one_le_A {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [μ.IsDoubling A] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [Nonempty X] [μ.IsOpenPosMeasure] : 1 ≤ A

theorem MeasureTheory.A_pos {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [μ.IsDoubling A] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [Nonempty X] [μ.IsOpenPosMeasure] : 0 < A

theorem MeasureTheory.A_pos' {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [μ.IsDoubling A] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [Nonempty X] [μ.IsOpenPosMeasure] : 0 < ↑A

theorem MeasureTheory.measure_ball_four_le_same {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] (x : X) (r : ℝ) : μ.real (Metric.ball x (4 * r)) ≤ ↑A ^ 2 * μ.real (Metric.ball x r)

theorem MeasureTheory.measure_ball_ne_top {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] (x : X) (r : ℝ) : μ (Metric.ball x r) ≠ ⊤

theorem MeasureTheory.measure_ball_four_le_same' {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] (x : X) (r : ℝ) : μ (Metric.ball x (4 * r)) ≤ ↑A ^ 2 * μ (Metric.ball x r)

theorem MeasureTheory.measure_ball_le_pow_two {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] {x : X} {r : ℝ} {n : ℕ} : μ.real (Metric.ball x (2 ^ n * r)) ≤ ↑A ^ n * μ.real (Metric.ball x r)

theorem MeasureTheory.measure_ball_le_pow_two' {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] {x : X} {r : ℝ} {n : ℕ} : μ (Metric.ball x (2 ^ n * r)) ≤ ↑A ^ n * μ (Metric.ball x r)

def MeasureTheory.As (A : NNReal) (s : ℝ) : NNReal

The blow-up factor of repeatedly increasing the size of balls.

Equations

• MeasureTheory.As A s = A ^ ⌈Real.logb 2 s⌉₊

theorem MeasureTheory.As_pos {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [μ.IsDoubling A] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [Nonempty X] [μ.IsOpenPosMeasure] (s : ℝ) : 0 < MeasureTheory.As A s

theorem MeasureTheory.As_pos' {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] (μ : MeasureTheory.Measure X) [μ.IsDoubling A] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [Nonempty X] [μ.IsOpenPosMeasure] (s : ℝ) : 0 < ↑(MeasureTheory.As A s)

theorem MeasureTheory.measure_ball_le_same' {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] (x : X) {r s r' : ℝ} (hsp : 0 < s) (hs : r' ≤ s * r) : μ (Metric.ball x r') ≤ ↑(MeasureTheory.As A s) * μ (Metric.ball x r)

theorem MeasureTheory.measure_ball_le_same {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] (x : X) {r s r' : ℝ} (hsp : 0 < s) (hs : r' ≤ s * r) : μ.real (Metric.ball x r') ≤ ↑(MeasureTheory.As A s) * μ.real (Metric.ball x r)

theorem MeasureTheory.measure_ball_le_of_dist_le' {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] {x x' : X} {r r' s : ℝ} (hs : 0 < s) (h : dist x x' + r' ≤ s * r) : μ (Metric.ball x' r') ≤ ↑(MeasureTheory.As A s) * μ (Metric.ball x r)

theorem MeasureTheory.measureNNReal_ball_le_of_dist_le' {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] {x x' : X} {r r' s : ℝ} (hs : 0 < s) (h : dist x x' + r' ≤ s * r) : μ.nnreal (Metric.ball x' r') ≤ MeasureTheory.As A s * μ.nnreal (Metric.ball x r)

def MeasureTheory.Ai (A : NNReal) (s : ℝ) : NNReal

Equations

• MeasureTheory.Ai A s = MeasureTheory.As A s

theorem MeasureTheory.measure_ball_le_of_subset {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] {x' x : X} {r r' s : ℝ} (hs : r' ≤ s * r) (hr : Metric.ball x' r ⊆ Metric.ball x r') : μ.real (Metric.ball x (2 * r)) ≤ ↑(MeasureTheory.Ai A s) * μ.real (Metric.ball x' r)

def MeasureTheory.Ai2 (A : NNReal) : NNReal

Equations

• MeasureTheory.Ai2 A = MeasureTheory.Ai A 2

theorem MeasureTheory.measure_ball_two_le_of_subset {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] {x' x : X} {r : ℝ} (hr : Metric.ball x' r ⊆ Metric.ball x (2 * r)) : μ.real (Metric.ball x (2 * r)) ≤ ↑(MeasureTheory.Ai2 A) * μ.real (Metric.ball x' r)

def MeasureTheory.Np (A : NNReal) (s : ℝ) : ℕ

Equations

• MeasureTheory.Np A s = ⌊MeasureTheory.As A (s * ↑A + 2⁻¹)⌋₊

theorem MeasureTheory.card_le_of_le_dist {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] [ProperSpace X] (x : X) {r r' s : ℝ} (P : Set X) (hs : r' ≤ s * r) (hP : P ⊆ Metric.ball x r') (h2P : ∀ (x y : X), x ∈ P → y ∈ P → x ≠ y → r ≤ dist x y) : P.Finite ∧ Nat.card ↑P ≤ MeasureTheory.Np A s

theorem MeasureTheory.ballsCoverBalls {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] [ProperSpace X] {r r' s : ℝ} (hs : r' ≤ s * r) : BallsCoverBalls X r' r (MeasureTheory.Np A s)

theorem MeasureTheory.continuous_measure_ball_inter {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] {U : Set X} (hU : IsOpen U) {δ : ℝ} (hδ : 0 < δ) : Continuous fun (x : X) => μ.real (Metric.ball x δ ∩ U)

theorem MeasureTheory.continuous_average {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} (hf : MeasureTheory.LocallyIntegrable f μ) {δ : ℝ} (hδ : 0 < δ) : Continuous fun (x : X) => ⨍ (y : X) in Metric.ball x δ, f y ∂μ

theorem MeasureTheory.tendsto_average_zero {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [ProperSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : X → E} (hf : MeasureTheory.LocallyIntegrable f μ) {x : X} : Filter.Tendsto (fun (δ : ℝ) => ⨍ (y : X) in Metric.ball x δ, f y ∂μ) (nhdsWithin 0 (Set.Ioi 0)) (nhds (f x))

instance MeasureTheory.instIsUnifLocDoublingMeasure_carleson {X : Type u_1} {A : NNReal} [MetricSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} [μ.IsDoubling A] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [ProperSpace X] [μ.IsOpenPosMeasure] : IsUnifLocDoublingMeasure μ

Equations

• ⋯ = ⋯

theorem MeasureTheory.Subsingleton.ball_eq {α : Type u_1} [PseudoMetricSpace α] [Subsingleton α] {x : α} {r : ℝ} : Metric.ball x r = if r > 0 then {x} else ∅

instance MeasureTheory.InnerProductSpace.IsDoubling {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] : MeasureTheory.volume.IsDoubling (2 ^ Module.finrank ℝ E)

Equations

• ⋯ = ⋯

class MeasureTheory.DoublingMeasure (X : Type u_1) (A : outParam NNReal) [PseudoMetricSpace X] extends MeasureTheory.MeasureSpace X, ProperSpace X, BorelSpace X, MeasureTheory.volume.Regular, MeasureTheory.volume.IsOpenPosMeasure, MeasureTheory.volume.IsDoubling A : Type u_1

A metric space with a measure and a doubling condition. This is called a "doubling metric measure space" in the blueprint. A will usually be 2 ^ a.

This class is not Mathlib-ready code, and results moved to Mathlib should be reformulated using a (locally) doubling measure and more minimal other classes.

Note (F): we currently assume that the space is proper, which we should probably add to the blueprint. Remark: IsUnifLocDoublingMeasure which is a weaker notion in Mathlib.

• MeasurableSet' : Set X → Prop
• measurableSet_empty : MeasureTheory.MeasureSpace.toMeasurableSpace.MeasurableSet' ∅
• measurableSet_compl : ∀ (s : Set X), MeasureTheory.MeasureSpace.toMeasurableSpace.MeasurableSet' s → MeasureTheory.MeasureSpace.toMeasurableSpace.MeasurableSet' sᶜ
• measurableSet_iUnion : ∀ (f : ℕ → Set X), (∀ (i : ℕ), MeasureTheory.MeasureSpace.toMeasurableSpace.MeasurableSet' (f i)) → MeasureTheory.MeasureSpace.toMeasurableSpace.MeasurableSet' (⋃ (i : ℕ), f i)
• volume : MeasureTheory.Measure X
• isCompact_closedBall : ∀ (x : X) (r : ℝ), IsCompact (Metric.closedBall x r)
• measurable_eq : MeasureTheory.MeasureSpace.toMeasurableSpace = borel X
• lt_top_of_isCompact : ∀ ⦃K : Set X⦄, IsCompact K → MeasureTheory.volume K < ⊤
• outerRegular : ∀ ⦃A_1 : Set X⦄, MeasurableSet A_1 → ∀ r > MeasureTheory.volume A_1, ∃ U ⊇ A_1, IsOpen U ∧ MeasureTheory.volume U < r
• innerRegular : MeasureTheory.volume.InnerRegularWRT IsCompact IsOpen
• open_pos : ∀ (U : Set X), IsOpen U → U.Nonempty → MeasureTheory.volume U ≠ 0
• measure_ball_two_le_same : ∀ (x : X) (r : ℝ), MeasureTheory.volume (Metric.ball x (2 * r)) ≤ ↑A * MeasureTheory.volume (Metric.ball x r)

@[reducible]

def MeasureTheory.DoublingMeasure.mono {X : Type u_1} {A : NNReal} [PseudoMetricSpace X] [MeasureTheory.DoublingMeasure X A] {A' : NNReal} (h : A ≤ A') : MeasureTheory.DoublingMeasure X A'

Monotonicity of doubling measure metric spaces in A.

Equations

• MeasureTheory.DoublingMeasure.mono h = MeasureTheory.DoublingMeasure.mk

instance MeasureTheory.InnerProductSpace.DoublingMeasure {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] : MeasureTheory.DoublingMeasure E (2 ^ Module.finrank ℝ E)

Equations

• MeasureTheory.InnerProductSpace.DoublingMeasure = MeasureTheory.DoublingMeasure.mk