Actual finite iid sampled-distance laws

The law is the pushforward of the full product probability measure by the literal distance matrix. Repeated sampled points remain possible. Measured isometries preserve the law, so it is defined on the source whole-space measured-isometry quotient. On a fixed metric carrier it varies continuously with the sampling probability measure.

Adapted from Freezing2/Probability/SampledDistanceLaw.lean in igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit 8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).

def BGW.MetricMeasure.distanceMatrix {X : Type u_1} [PseudoMetricSpace X] (k : ℕ) (v : Fin k → X) : Fin k → Fin k → ℝ

Distances between all sampled points, with the exact zero diagonal.

Equations

• BGW.MetricMeasure.distanceMatrix k v i j = dist (v i) (v j)

@[simp]

theorem BGW.MetricMeasure.distanceMatrix_diag {X : Type u_1} [PseudoMetricSpace X] (k : ℕ) (v : Fin k → X) (i : Fin k) : distanceMatrix k v i i = 0

theorem BGW.MetricMeasure.continuous_distanceMatrix {X : Type u_1} [PseudoMetricSpace X] (k : ℕ) : Continuous (distanceMatrix k)

noncomputable def BGW.MetricMeasure.iidDistanceLawOn {X : Type u_1} [MetricSpace X] [MeasurableSpace X] (μ : MeasureTheory.ProbabilityMeasure X) (k : ℕ) : MeasureTheory.ProbabilityMeasure (Fin k → Fin k → ℝ)

The genuine iid distance-matrix law, including collisions and k=0.

Equations

• BGW.MetricMeasure.iidDistanceLawOn μ k = (MeasureTheory.ProbabilityMeasure.pi fun (x : Fin k) => μ).map (BGW.MetricMeasure.distanceMatrix k)

theorem BGW.MetricMeasure.continuous_iidDistanceLawOn {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X] (k : ℕ) : Continuous fun (μ : MeasureTheory.ProbabilityMeasure X) => iidDistanceLawOn μ k

Fixed-carrier weak convergence of sampling measures gives weak convergence of the entire finite sampled-distance matrix.

theorem BGW.MetricMeasure.iidDistanceLawOn_map_isometry {X : Type u_1} {Y : Type u_2} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [SecondCountableTopology Y] (μ : MeasureTheory.ProbabilityMeasure X) (f : X → Y) (hf : Isometry f) (k : ℕ) : iidDistanceLawOn (μ.map f) k = iidDistanceLawOn μ k

Isometric mapping of the sampling measure preserves the sampled law.

noncomputable def BGW.MetricMeasure.iidDistanceLaw (X : CompactMeasuredSpace) (k : ℕ) : MeasureTheory.ProbabilityMeasure (Fin k → Fin k → ℝ)

The finite iid matrix law of a represented compact measured space.

Equations

• BGW.MetricMeasure.iidDistanceLaw X k = BGW.MetricMeasure.iidDistanceLawOn X.law k

theorem BGW.MetricMeasure.iidDistanceLaw_eq_of_measuredIsometry {X Y : CompactMeasuredSpace} (h : X.MeasuredIsometry Y) (k : ℕ) : iidDistanceLaw X k = iidDistanceLaw Y k

Whole-space measured isometry leaves every finite sampled law unchanged.

noncomputable def BGW.MetricMeasure.MeasuredGHSpace.sampledDistanceLaw (k : ℕ) : MeasuredGHSpace → MeasureTheory.ProbabilityMeasure (Fin k → Fin k → ℝ)

The sampled-distance law on the source quotient. No sample distinctness or full-support condition is added by passage to isometry classes.

Equations

• BGW.MetricMeasure.MeasuredGHSpace.sampledDistanceLaw k = Quotient.lift (fun (X : BGW.MetricMeasure.CompactMeasuredSpace) => BGW.MetricMeasure.iidDistanceLaw X k) ⋯

@[simp]

theorem BGW.MetricMeasure.MeasuredGHSpace.sampledDistanceLaw_toMeasuredGHSpace (X : CompactMeasuredSpace) (k : ℕ) : sampledDistanceLaw k (toMeasuredGHSpace X) = iidDistanceLaw X k