A copy of a metric space with metric given by d x y = dist x y ^ α

Given a (pseudo) (extended) metric space X and a number 0 < α < 1, one can consider the metric given by d x y = (dist x y) ^ α. In this file we define WithRPowDist X α hα₀ hα₁ to be a one-field structure wrapper around X with metric given by this formula.

One of the reasons to introduce this definition is the following. In the proof of his version of the Morse-Sard theorem, Moreira [Moreira2001] studies maps of two variables that are Lipschitz continuous in one variable, but satisfy a stronger assumption ‖f (a, y) - f (a, b)‖ = O(‖y - b‖ ^ α) along the second variable, as long as (a, b) is one of the "interesting" points.

If we want to apply Vitali family in this context, we need to cover the set by products closedBall a (R ^ α) ×ˢ closedBall b R so that both components make a similar contribution to ‖f (x, y) - f (a, b)‖. These sets aren't balls in the original metric (or even subsets of balls that occupy at least a fixed fraction of the volume, as we require in our version of Vitali theorem).

However, if we change the metric on the first component to the one introduced in this file, then these sets become balls, and we can apply Vitali theorem.

References

• [Carlos Gustavo T. de A. Moreira, Hausdorff measures and the Morse-Sard theorem] [Moreira2001]

structure WithRPowDist (X : Type u_1) (α : ℝ) (hα₀ : 0 < α) (hα₁ : α ≤ 1) : Type u_1

A copy of a type with metric given by dist x y = (dist x.val y.val) ^ α.

This is defined as a one-field structure.

• val : X

  The value wrapped in x : WithRPowDist X α hα₀ hα₁.

theorem WithRPowDist.ext_iff {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} {x y : WithRPowDist X α hα₀ hα₁} : x = y ↔ x.val = y.val

theorem WithRPowDist.ext {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} {x y : WithRPowDist X α hα₀ hα₁} (val : x.val = y.val) : x = y

def WithRPowDist.equiv (X : Type u_2) (α : ℝ) (hr₀ : 0 < α) (hr₁ : α ≤ 1) : WithRPowDist X α hr₀ hr₁ ≃ X

The natural equivalence between WithRPowDist X α hr₀ hr₁ and X.

Equations

• WithRPowDist.equiv X α hr₀ hr₁ = { toFun := WithRPowDist.val, invFun := WithRPowDist.mk, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem WithRPowDist.equiv_symm_apply (X : Type u_2) (α : ℝ) (hr₀ : 0 < α) (hr₁ : α ≤ 1) : ⇑(equiv X α hr₀ hr₁).symm = mk

@[simp]

theorem WithRPowDist.equiv_apply (X : Type u_2) (α : ℝ) (hr₀ : 0 < α) (hr₁ : α ≤ 1) : ⇑(equiv X α hr₀ hr₁) = val

@[simp]

theorem WithRPowDist.val_comp_mk {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} : val ∘ mk = id

@[simp]

theorem WithRPowDist.mk_comp_val {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} : mk ∘ val = id

theorem WithRPowDist.image_mk_eq_preimage {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} (s : Set X) : mk '' s = val ⁻¹' s

theorem WithRPowDist.image_val_eq_preimage {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} (s : Set (WithRPowDist X α hα₀ hα₁)) : val '' s = mk ⁻¹' s

@[simp]

theorem WithRPowDist.image_mk_image_val {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} (s : Set (WithRPowDist X α hα₀ hα₁)) : mk '' val '' s = s

@[simp]

theorem WithRPowDist.image_val_image_mk {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} (s : Set X) : val '' mk '' s = s

theorem WithRPowDist.surjective_val {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} : Function.Surjective val

theorem WithRPowDist.surjective_mk {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} : Function.Surjective mk

theorem WithRPowDist.injective_mk {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} : Function.Injective mk

Topological space structure

The topology on WithRPowDist X α hα₀ hα₁ is induced from X.

@[implicit_reducible]

instance WithRPowDist.instTopologicalSpace {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [TopologicalSpace X] : TopologicalSpace (WithRPowDist X α hα₀ hα₁)

The topological space structure on WithRPowDist X α _ _ is induced from the original space.

Equations

• WithRPowDist.instTopologicalSpace = TopologicalSpace.induced WithRPowDist.val inst✝

theorem WithRPowDist.continuous_val {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [TopologicalSpace X] : Continuous val

theorem WithRPowDist.continuous_mk {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [TopologicalSpace X] : Continuous mk

def WithRPowDist.homeomorph {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [TopologicalSpace X] : WithRPowDist X α hα₀ hα₁ ≃ₜ X

The natural homeomorphism between WithRPowDist X α hα₀ hα₁ and X.

Equations

• WithRPowDist.homeomorph = { toEquiv := WithRPowDist.equiv X α hα₀ hα₁, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem WithRPowDist.homeomorph_symm_apply {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [TopologicalSpace X] : ⇑homeomorph.symm = mk

@[simp]

theorem WithRPowDist.toEquiv_homeomorph {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [TopologicalSpace X] : homeomorph.toEquiv = equiv X α hα₀ hα₁

@[simp]

theorem WithRPowDist.homeomorph_apply {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [TopologicalSpace X] : ⇑homeomorph = val

We copy some instances from the underlying space X to WithRPowDist X α hα₀ hα₁. In the future, we can add more of them, if needed, or even copy all the topology-related classes, if we get a tactic to do it automatically.

instance WithRPowDist.instT0Space {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [TopologicalSpace X] [T0Space X] : T0Space (WithRPowDist X α hα₀ hα₁)

instance WithRPowDist.instT2Space {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [TopologicalSpace X] [T2Space X] : T2Space (WithRPowDist X α hα₀ hα₁)

instance WithRPowDist.instSecondCountableTopology {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [TopologicalSpace X] [SecondCountableTopology X] : SecondCountableTopology (WithRPowDist X α hα₀ hα₁)

Bornology

The bornology on WithRPowDist X α hα₀ hα₁ is induced from X.

@[implicit_reducible]

instance WithRPowDist.instBornology {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [Bornology X] : Bornology (WithRPowDist X α hα₀ hα₁)

Equations

• WithRPowDist.instBornology = Bornology.induced WithRPowDist.val

@[simp]

theorem WithRPowDist.isBounded_image_val_iff {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [Bornology X] {s : Set (WithRPowDist X α hα₀ hα₁)} : Bornology.IsBounded (val '' s) ↔ Bornology.IsBounded s

@[simp]

theorem WithRPowDist.isBounded_preimage_mk_iff {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [Bornology X] {s : Set (WithRPowDist X α hα₀ hα₁)} : Bornology.IsBounded (mk ⁻¹' s) ↔ Bornology.IsBounded s

@[simp]

theorem WithRPowDist.isBounded_image_mk_iff {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [Bornology X] {s : Set X} : Bornology.IsBounded (mk '' s) ↔ Bornology.IsBounded s

@[simp]

theorem WithRPowDist.isBounded_preimage_val_iff {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [Bornology X] {s : Set X} : Bornology.IsBounded (val ⁻¹' s) ↔ Bornology.IsBounded s

Uniform space structure

The uniform space structure on WithRPowDist X α hα₀ hα₁ is induced from X.

@[implicit_reducible]

instance WithRPowDist.instUniformSpace {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [UniformSpace X] : UniformSpace (WithRPowDist X α hα₀ hα₁)

Equations

• WithRPowDist.instUniformSpace = UniformSpace.comap WithRPowDist.val inst✝

theorem WithRPowDist.uniformContinuous_val {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [UniformSpace X] : UniformContinuous val

theorem WithRPowDist.uniformContinuous_mk {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [UniformSpace X] : UniformContinuous mk

def WithRPowDist.uniformEquiv {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [UniformSpace X] : WithRPowDist X α hα₀ hα₁ ≃ᵤ X

The natural uniform equivalence between WithRPowDist X α hα₀ hα₁ and X.

Equations

• WithRPowDist.uniformEquiv = { toEquiv := WithRPowDist.equiv X α hα₀ hα₁, uniformContinuous_toFun := ⋯, uniformContinuous_invFun := ⋯ }

@[simp]

theorem WithRPowDist.uniformEquiv_symm_apply {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [UniformSpace X] (val : X) : uniformEquiv.symm val = { val := val }

@[simp]

theorem WithRPowDist.uniformEquiv_apply {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [UniformSpace X] (self : WithRPowDist X α hα₀ hα₁) : uniformEquiv self = self.val

@[simp]

theorem WithRPowDist.uniformEquiv_toEquiv {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [UniformSpace X] : uniformEquiv.toEquiv = equiv X α hα₀ hα₁

Extended distance and a (pseudo) extended metric space structure

Th extended distance on WithRPowDist X α hα₀ hα₁ is given by edist x y = (edist x.val y.val) ^ α.

If the original space is a (pseudo) extended metric space, then so is WithRPowDist X α hα₀ hα₁.

@[implicit_reducible]

noncomputable instance WithRPowDist.instEDist {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [EDist X] : EDist (WithRPowDist X α hα₀ hα₁)

Equations

• WithRPowDist.instEDist = { edist := fun (x y : WithRPowDist X α hα₀ hα₁) => edist x.val y.val ^ α }

theorem WithRPowDist.edist_def {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [EDist X] (x y : WithRPowDist X α hα₀ hα₁) : edist x y = edist x.val y.val ^ α

@[simp]

theorem WithRPowDist.edist_mk_mk {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [EDist X] (x y : X) : edist { val := x } { val := y } = edist x y ^ α

@[simp]

theorem WithRPowDist.edist_val_val {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [EDist X] (x y : WithRPowDist X α hα₀ hα₁) : edist x.val y.val = edist x y ^ α⁻¹

@[implicit_reducible]

noncomputable instance WithRPowDist.instPseudoEMetricSpace {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoEMetricSpace X] : PseudoEMetricSpace (WithRPowDist X α hα₀ hα₁)

Equations

• WithRPowDist.instPseudoEMetricSpace = { toEDist := WithRPowDist.instEDist, edist_self := ⋯, edist_comm := ⋯, edist_triangle := ⋯, toUniformSpace := inferInstance, uniformity_edist := ⋯ }

@[simp]

theorem WithRPowDist.preimage_val_emetricBall {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoEMetricSpace X] (x : X) (r : ENNReal) : val ⁻¹' Metric.eball x r = Metric.eball { val := x } (r ^ α)

@[simp]

theorem WithRPowDist.image_mk_emetricBall {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoEMetricSpace X] (x : X) (r : ENNReal) : mk '' Metric.eball x r = Metric.eball { val := x } (r ^ α)

@[simp]

theorem WithRPowDist.preimage_mk_emetricBall {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoEMetricSpace X] (x : WithRPowDist X α hα₀ hα₁) (d : ENNReal) : mk ⁻¹' Metric.eball x d = Metric.eball x.val (d ^ α⁻¹)

@[simp]

theorem WithRPowDist.image_val_emetricBall {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoEMetricSpace X] (x : WithRPowDist X α hα₀ hα₁) (d : ENNReal) : val '' Metric.eball x d = Metric.eball x.val (d ^ α⁻¹)

@[simp]

theorem WithRPowDist.preimage_val_emetricClosedBall {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoEMetricSpace X] (x : X) (r : ENNReal) : val ⁻¹' Metric.closedEBall x r = Metric.closedEBall { val := x } (r ^ α)

@[simp]

theorem WithRPowDist.image_mk_emetricClosedBall {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoEMetricSpace X] (x : X) (r : ENNReal) : mk '' Metric.closedEBall x r = Metric.closedEBall { val := x } (r ^ α)

@[simp]

theorem WithRPowDist.preimage_mk_emetricClosedBall {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoEMetricSpace X] (x : WithRPowDist X α hα₀ hα₁) (d : ENNReal) : mk ⁻¹' Metric.closedEBall x d = Metric.closedEBall x.val (d ^ α⁻¹)

@[simp]

theorem WithRPowDist.image_val_emetricClosedBall {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoEMetricSpace X] (x : WithRPowDist X α hα₀ hα₁) (d : ENNReal) : val '' Metric.closedEBall x d = Metric.closedEBall x.val (d ^ α⁻¹)

@[simp]

theorem WithRPowDist.ediam_image_val {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoEMetricSpace X] (s : Set (WithRPowDist X α hα₀ hα₁)) : Metric.ediam (val '' s) = Metric.ediam s ^ α⁻¹

@[simp]

theorem WithRPowDist.ediam_preimage_mk {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoEMetricSpace X] (s : Set (WithRPowDist X α hα₀ hα₁)) : Metric.ediam (mk ⁻¹' s) = Metric.ediam s ^ α⁻¹

@[simp]

theorem WithRPowDist.ediam_preimage_val {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoEMetricSpace X] (s : Set X) : Metric.ediam (val ⁻¹' s) = Metric.ediam s ^ α

@[simp]

theorem WithRPowDist.ediam_image_mk {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoEMetricSpace X] (s : Set X) : Metric.ediam (mk '' s) = Metric.ediam s ^ α

@[implicit_reducible]

noncomputable instance WithRPowDist.instEMetricSpace {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [EMetricSpace X] : EMetricSpace (WithRPowDist X α hα₀ hα₁)

Equations

• WithRPowDist.instEMetricSpace = EMetricSpace.ofT0PseudoEMetricSpace (WithRPowDist X α hα₀ hα₁)

Distance and a (pseudo) metric space structure

Th extended distance on WithRPowDist X α hα₀ hα₁ is given by dist x y = (dist x.val y.val) ^ α.

If the original space is a (pseudo) metric space, then so is WithRPowDist X α hα₀ hα₁.

@[implicit_reducible]

noncomputable instance WithRPowDist.instDist {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [Dist X] : Dist (WithRPowDist X α hα₀ hα₁)

Equations

• WithRPowDist.instDist = { dist := fun (x y : WithRPowDist X α hα₀ hα₁) => dist x.val y.val ^ α }

@[simp]

theorem WithRPowDist.dist_mk_mk {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [Dist X] (x y : X) : dist { val := x } { val := y } = dist x y ^ α

@[implicit_reducible]

noncomputable instance WithRPowDist.instPseudoMetricSpace {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoMetricSpace X] : PseudoMetricSpace (WithRPowDist X α hα₀ hα₁)

Equations

• WithRPowDist.instPseudoMetricSpace = (PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯).replaceBornology ⋯

@[simp]

theorem WithRPowDist.dist_val_val {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoMetricSpace X] (x y : WithRPowDist X α hα₀ hα₁) : dist x.val y.val = dist x y ^ α⁻¹

@[simp]

theorem WithRPowDist.preimage_val_ball {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoMetricSpace X] (x : X) {r : ℝ} (hr : 0 ≤ r) : val ⁻¹' Metric.ball x r = Metric.ball { val := x } (r ^ α)

@[simp]

theorem WithRPowDist.image_mk_ball {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoMetricSpace X] (x : X) {r : ℝ} (hr : 0 ≤ r) : mk '' Metric.ball x r = Metric.ball { val := x } (r ^ α)

@[simp]

theorem WithRPowDist.preimage_mk_ball {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoMetricSpace X] (x : WithRPowDist X α hα₀ hα₁) {r : ℝ} (hr : 0 ≤ r) : mk ⁻¹' Metric.ball x r = Metric.ball x.val (r ^ α⁻¹)

@[simp]

theorem WithRPowDist.image_val_ball {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoMetricSpace X] (x : WithRPowDist X α hα₀ hα₁) {r : ℝ} (hr : 0 ≤ r) : val '' Metric.ball x r = Metric.ball x.val (r ^ α⁻¹)

@[simp]

theorem WithRPowDist.preimage_val_closedBall {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoMetricSpace X] (x : X) {r : ℝ} (hr : 0 ≤ r) : val ⁻¹' Metric.closedBall x r = Metric.closedBall { val := x } (r ^ α)

@[simp]

theorem WithRPowDist.image_mk_closedBall {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoMetricSpace X] (x : X) {r : ℝ} (hr : 0 ≤ r) : mk '' Metric.closedBall x r = Metric.closedBall { val := x } (r ^ α)

@[simp]

theorem WithRPowDist.preimage_mk_closedBall {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoMetricSpace X] (x : WithRPowDist X α hα₀ hα₁) {r : ℝ} (hr : 0 ≤ r) : mk ⁻¹' Metric.closedBall x r = Metric.closedBall x.val (r ^ α⁻¹)

@[simp]

theorem WithRPowDist.image_val_closedBall {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [PseudoMetricSpace X] (x : WithRPowDist X α hα₀ hα₁) {r : ℝ} (hr : 0 ≤ r) : val '' Metric.closedBall x r = Metric.closedBall x.val (r ^ α⁻¹)

@[implicit_reducible]

noncomputable instance WithRPowDist.instMetricSpace {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [MetricSpace X] : MetricSpace (WithRPowDist X α hα₀ hα₁)

Equations

• WithRPowDist.instMetricSpace = MetricSpace.ofT0PseudoMetricSpace (WithRPowDist X α hα₀ hα₁)