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

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

Equations

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

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_ball_four_le_same {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] {μ : Measure X} [μ.IsDoubling A] (x : X) (r : ℝ) : μ (Metric.ball x (4 * r)) ≤ ↑A ^ 2 * μ (Metric.ball x r)

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_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.isOpenPosMeasure_of_isDoubling {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] (μ : Measure X) [μ.IsDoubling A] [NeZero μ] : μ.IsOpenPosMeasure

instance MeasureTheory.instIsUnifLocDoublingMeasure_carleson {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] {μ : Measure X} [μ.IsDoubling A] : IsUnifLocDoublingMeasure μ

theorem MeasureTheory.Nat.exists_max_image {α : Type u_2} {s : Set α} (hs : s.Nonempty) {f : α → ℕ} (h : BddAbove (f '' s)) : ∃ x ∈ s, ∀ y ∈ s, f y ≤ f x

theorem MeasureTheory.IsDoubling.measure_ball_lt_top {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] {μ : Measure X} [μ.IsDoubling A] [IsLocallyFiniteMeasure μ] {x : X} {r : ℝ} : μ (Metric.ball x r) < ⊤

theorem MeasureTheory.IsDoubling.allBallsCoverBalls {X : Type u_1} [PseudoMetricSpace X] {A : NNReal} [MeasurableSpace X] (μ : Measure X) [μ.IsDoubling A] [OpensMeasurableSpace X] [NeZero μ] [IsLocallyFiniteMeasure μ] : AllBallsCoverBalls X 2 ⌈As A 9⌉₊

theorem MeasureTheory.measureReal_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.measureReal_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.measureReal_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.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.measureReal_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.measureReal_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.measureReal_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 measureReal_ball_le_same without ceiling function.

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) : (μ (Metric.ball x' r')).toNNReal ≤ As A s * (μ (Metric.ball x r)).toNNReal

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)