Uniformly locally doubling measures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A uniformly locally doubling measure μ on a metric space is a measure for which there exists a constant C such that for all sufficiently small radii ε, and for any centre, the measure of a ball of radius 2 * ε is bounded by C times the measure of the concentric ball of radius ε.

This file records basic facts about uniformly locally doubling measures.

Main definitions #

is_unif_loc_doubling_measure: the definition of a uniformly locally doubling measure (as a typeclass).
is_unif_loc_doubling_measure.doubling_constant: a function yielding the doubling constant C appearing in the definition of a uniformly locally doubling measure.

source

@[class]

structure is_unif_loc_doubling_measure {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) :

Type

exists_measure_closed_ball_le_mul : ∃ (C : nnreal), ∀ᶠ (ε : ℝ) in nhds_within 0 (set.Ioi 0), ∀ (x : α), ⇑μ (metric.closed_ball x (2 * ε)) ≤ ↑C * ⇑μ (metric.closed_ball x ε)

A measure μ is said to be a uniformly locally doubling measure if there exists a constant C such that for all sufficiently small radii ε, and for any centre, the measure of a ball of radius 2 * ε is bounded by C times the measure of the concentric ball of radius ε.

Note: it is important that this definition makes a demand only for sufficiently small ε. For example we want hyperbolic space to carry the instance is_unif_loc_doubling_measure volume but volumes grow exponentially in hyperbolic space. To be really explicit, consider the hyperbolic plane of curvature -1, the area of a disc of radius ε is A(ε) = 2π(cosh(ε) - 1) so A(2ε)/A(ε) ~ exp(ε).

Instances of this typeclass

Instances of other typeclasses for is_unif_loc_doubling_measure

is_unif_loc_doubling_measure.has_sizeof_inst

source

noncomputable def is_unif_loc_doubling_measure.doubling_constant {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_unif_loc_doubling_measure μ] :

nnreal

A doubling constant for a uniformly locally doubling measure.

Equations

is_unif_loc_doubling_measure.doubling_constant μ = classical.some _

source

theorem is_unif_loc_doubling_measure.exists_measure_closed_ball_le_mul' {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_unif_loc_doubling_measure μ] :

∀ᶠ (ε : ℝ) in nhds_within 0 (set.Ioi 0), ∀ (x : α), ⇑μ (metric.closed_ball x (2 * ε)) ≤ ↑(is_unif_loc_doubling_measure.doubling_constant μ) * ⇑μ (metric.closed_ball x ε)

source

theorem is_unif_loc_doubling_measure.exists_eventually_forall_measure_closed_ball_le_mul {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_unif_loc_doubling_measure μ] (K : ℝ) :

∃ (C : nnreal), ∀ᶠ (ε : ℝ) in nhds_within 0 (set.Ioi 0), ∀ (x : α) (t : ℝ), t ≤ K → ⇑μ (metric.closed_ball x (t * ε)) ≤ ↑C * ⇑μ (metric.closed_ball x ε)

source

noncomputable def is_unif_loc_doubling_measure.scaling_constant_of {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_unif_loc_doubling_measure μ] (K : ℝ) :

nnreal

A variant of is_unif_loc_doubling_measure.doubling_constant which allows for scaling the radius by values other than 2.

Equations

is_unif_loc_doubling_measure.scaling_constant_of μ K = linear_order.max (classical.some _) 1

source

@[simp]

theorem is_unif_loc_doubling_measure.one_le_scaling_constant_of {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_unif_loc_doubling_measure μ] (K : ℝ) :

1 ≤ is_unif_loc_doubling_measure.scaling_constant_of μ K

source

theorem is_unif_loc_doubling_measure.eventually_measure_mul_le_scaling_constant_of_mul {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_unif_loc_doubling_measure μ] (K : ℝ) :

∃ (R : ℝ), 0 < R ∧ ∀ (x : α) (t r : ℝ), t ∈ set.Ioc 0 K → r ≤ R → ⇑μ (metric.closed_ball x (t * r)) ≤ ↑(is_unif_loc_doubling_measure.scaling_constant_of μ K) * ⇑μ (metric.closed_ball x r)

source

theorem is_unif_loc_doubling_measure.eventually_measure_le_scaling_constant_mul {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_unif_loc_doubling_measure μ] (K : ℝ) :

∀ᶠ (r : ℝ) in nhds_within 0 (set.Ioi 0), ∀ (x : α), ⇑μ (metric.closed_ball x (K * r)) ≤ ↑(is_unif_loc_doubling_measure.scaling_constant_of μ K) * ⇑μ (metric.closed_ball x r)

source

theorem is_unif_loc_doubling_measure.eventually_measure_le_scaling_constant_mul' {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_unif_loc_doubling_measure μ] (K : ℝ) (hK : 0 < K) :

∀ᶠ (r : ℝ) in nhds_within 0 (set.Ioi 0), ∀ (x : α), ⇑μ (metric.closed_ball x r) ≤ ↑(is_unif_loc_doubling_measure.scaling_constant_of μ K⁻¹) * ⇑μ (metric.closed_ball x (K * r))

source

noncomputable def is_unif_loc_doubling_measure.scaling_scale_of {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_unif_loc_doubling_measure μ] (K : ℝ) :

ℝ

A scale below which the doubling measure μ satisfies good rescaling properties when one multiplies the radius of balls by at most K, as stated in measure_mul_le_scaling_constant_of_mul.

Equations

is_unif_loc_doubling_measure.scaling_scale_of μ K = _.some

source

theorem is_unif_loc_doubling_measure.scaling_scale_of_pos {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_unif_loc_doubling_measure μ] (K : ℝ) :

0 < is_unif_loc_doubling_measure.scaling_scale_of μ K

source

theorem is_unif_loc_doubling_measure.measure_mul_le_scaling_constant_of_mul {α : Type u_1} [metric_space α] [measurable_space α] (μ : measure_theory.measure α) [is_unif_loc_doubling_measure μ] {K : ℝ} {x : α} {t r : ℝ} (ht : t ∈ set.Ioc 0 K) (hr : r ≤ is_unif_loc_doubling_measure.scaling_scale_of μ K) :

⇑μ (metric.closed_ball x (t * r)) ≤ ↑(is_unif_loc_doubling_measure.scaling_constant_of μ K) * ⇑μ (metric.closed_ball x r)