Direct sum of metric spaces

This files endows the direct sum ι →₀ X of ι-many copies of a metric space X with the L^p metric.

TODO

Allow the L^∞ metric too. Currently, there is no easy way to perform the proofs: match on ℝ≥0∞ exposes the underlying Option and induction p using ENNReal.recTopCoe in the EMetricSpace instance chokes on the PseudoEMetricSpace one.

@[implicit_reducible]

noncomputable instance Finsupp.instPseudoEMetricSpaceWithLpOfNNReal {ι : Type u_1} {X : Type u_2} [Zero X] {p : NNReal} [Fact (1 ≤ p)] [PseudoEMetricSpace X] : PseudoEMetricSpace (WithLp (↑p) (ι →₀ X))

The L^1 extended metric on ι-many copies of a metric space X

Equations

• One or more equations did not get rendered due to their size.

theorem Finsupp.edist_def {ι : Type u_1} {X : Type u_2} [Zero X] [PseudoEMetricSpace X] {p : NNReal} [Fact (1 ≤ p)] (f g : WithLp (↑p) (ι →₀ X)) : edist f g = ((zipWith edist ⋯ f.ofLp g.ofLp).sum fun (_i : ι) (r : ENNReal) => r ^ ↑p) ^ (↑p)⁻¹

@[implicit_reducible]

noncomputable instance Finsupp.instEMetricSpaceWithLpOfNNReal {ι : Type u_1} {X : Type u_2} [Zero X] {p : NNReal} [Fact (1 ≤ p)] [EMetricSpace X] : EMetricSpace (WithLp (↑p) (ι →₀ X))

The L^1 extended metric on ι-many copies of a metric space X

Equations

• Finsupp.instEMetricSpaceWithLpOfNNReal = { toPseudoEMetricSpace := Finsupp.instPseudoEMetricSpaceWithLpOfNNReal, eq_of_edist_eq_zero := ⋯ }

@[implicit_reducible]

noncomputable instance Finsupp.instPseudoMetricSpaceWithLpOfNNReal {ι : Type u_1} {X : Type u_2} [Zero X] {p : NNReal} [Fact (1 ≤ p)] [PseudoMetricSpace X] : PseudoMetricSpace (WithLp (↑p) (ι →₀ X))

The L^1 metric on ι-many copies of a metric space X

Equations

• One or more equations did not get rendered due to their size.

theorem Finsupp.dist_def {ι : Type u_1} {X : Type u_2} [Zero X] {p : NNReal} [Fact (1 ≤ p)] [PseudoMetricSpace X] (f g : WithLp (↑p) (ι →₀ X)) : dist f g = ((zipWith dist ⋯ f.ofLp g.ofLp).sum fun (_i : ι) (r : ℝ) => r ^ ↑p) ^ (↑p)⁻¹

theorem Finsupp.nndist_def {ι : Type u_1} {X : Type u_2} [Zero X] {p : NNReal} [Fact (1 ≤ p)] [PseudoMetricSpace X] (f g : WithLp (↑p) (ι →₀ X)) : nndist f g = ((zipWith nndist ⋯ f.ofLp g.ofLp).sum fun (_i : ι) (r : NNReal) => r ^ ↑p) ^ (↑p)⁻¹

@[implicit_reducible]

noncomputable instance Finsupp.instMetricSpaceWithLpOfNNReal {ι : Type u_1} {X : Type u_2} [Zero X] {p : NNReal} [Fact (1 ≤ p)] [MetricSpace X] : MetricSpace (WithLp (↑p) (ι →₀ X))

The L^1 metric on ι-many copies of a metric space X

Equations

• One or more equations did not get rendered due to their size.