class MeasureTheory.Measure.IsDoubling {X : Type u_1} [MeasurableSpace X] [PseudoMetricSpace X] (μ : 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.dist_lt_of_not_disjoint_ball {X : Type u_1} [PseudoMetricSpace X] {x x' : X} {r r' : ℝ} (hd : ¬Disjoint (Metric.ball x r) (Metric.ball x' r')) : dist x x' < r + r'

theorem MeasureTheory.eq_zero_of_isDoubling_zero {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] (μ : Measure X) [hμ : μ.IsDoubling 0] : μ = 0

theorem MeasureTheory.eq_zero_of_isDoubling_lt_one {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] (μ : Measure X) [μ.IsDoubling A] [ProperSpace X] [IsFiniteMeasureOnCompacts μ] (hA : A < 1) : μ = 0

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

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

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

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

theorem MeasureTheory.measure_real_ball_pos {X : Type u_1} [PseudoMetricSpace X] [MeasurableSpace X] {μ : Measure X} [ProperSpace X] [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] (μ : Measure X) [μ.IsDoubling A] [ProperSpace X] [IsFiniteMeasureOnCompacts μ] [Nonempty X] [μ.IsOpenPosMeasure] : 1 ≤ A

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

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

theorem MeasureTheory.measure_ball_four_le_same {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] {μ : Measure X} [μ.IsDoubling A] [ProperSpace X] [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] {μ : Measure X} [ProperSpace X] [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] {μ : Measure X} [μ.IsDoubling A] [ProperSpace X] [IsFiniteMeasureOnCompacts μ] (x : X) (r : ℝ) : μ (Metric.ball x (4 * r)) ≤ ↑A ^ 2 * μ (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] (μ : Measure X) [μ.IsDoubling A] [ProperSpace X] [IsFiniteMeasureOnCompacts μ] [Nonempty X] [μ.IsOpenPosMeasure] (s : ℝ) : 0 < As A s

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

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

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

theorem MeasureTheory.measure_ball_le_same'' {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] {μ : Measure X} [μ.IsDoubling A] [ProperSpace X] [IsFiniteMeasureOnCompacts μ] (x : X) {r t : ℝ} (ht : 0 < t) (h't : t ≤ 1) : μ.real (Metric.ball x r) ≤ ↑A * t ^ (-Real.logb 2 ↑A) * μ.real (Metric.ball x (t * r))

Version of measure_ball_le_same without ceiling function.

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

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

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] : volume.IsDoubling (2 ^ Module.finrank ℝ E)

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 : 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 → volume K < ⊤
• outerRegular ⦃A : Set X⦄ : MeasurableSet A → ∀ r > volume A, ∃ U ⊇ A, IsOpen U ∧ volume U < r
• innerRegular : volume.InnerRegularWRT IsCompact IsOpen
• open_pos (U : Set X) : IsOpen U → U.Nonempty → volume U ≠ 0
• measure_ball_two_le_same (x : X) (r : ℝ) : volume (Metric.ball x (2 * r)) ≤ ↑A * volume (Metric.ball x r)

@[reducible]

def MeasureTheory.DoublingMeasure.mono {X : Type u_1} {A : NNReal} [PseudoMetricSpace X] [DoublingMeasure X A] {A' : NNReal} (h : A ≤ A') : 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