Quantization.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem358.exists_measurable_ball_selector line 13

Source documentation

Select, measurably, a point of a finite family of balls covering the input. Outside their union the selector takes a fixed default value.

theorem exists_measurable_ball_selector
    {X : Type*} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X]
    (s : Finset X) (y₀ : X) (ε : ℝ) :
    ∃ Q : X → X, Measurable Q ∧
      (∀ x, Q x = y₀ ∨ Q x ∈ s) ∧
      (∀ x, (∃ y ∈ s, dist x y < ε) → dist x (Q x) < ε) := by
…

theorem OAI.Problem358.IsCompact.exists_measurable_finite_quantizer line 50

Source documentation

A compact nonempty set admits measurable finite-valued quantizers with arbitrarily small error. The quantizer takes values in the set even away from it.

theorem IsCompact.exists_measurable_finite_quantizer
    {X : Type*} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X]
    {Y : Set X} (hY : IsCompact Y) (hne : Y.Nonempty)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ Q : X → X, Measurable Q ∧ (Set.range Q).Finite ∧
      (∀ x, Q x ∈ Y) ∧ ∀ x ∈ Y, dist x (Q x) < ε := by
…

theorem OAI.Problem358.IsCompact.exists_finite_quantizer_sequence line 75

Source documentation

A single sequence of finite-valued Borel maps approximates the identity uniformly on a compact set, with a specified reciprocal error rate.

theorem IsCompact.exists_finite_quantizer_sequence
    {X : Type*} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X]
    {Y : Set X} (hY : IsCompact Y) (hne : Y.Nonempty) :
    ∃ Q : ℕ → X → X,
      (∀ n, Measurable (Q n)) ∧
      (∀ n, (Set.range (Q n)).Finite) ∧
      (∀ n x, Q n x ∈ Y) ∧
      (∀ n x, x ∈ Y → dist x (Q n x) < 1 / ((n : ℝ) + 1)) ∧
      TendstoUniformlyOn Q id Filter.atTop Y := by
…

theorem OAI.Problem358.tendsto_integral_comp_of_compact_quantizers line 97

Source documentation

Continuous test integrals are stable under compact-valued uniform quantization, for any finite measure concentrated on the compact set.

theorem tendsto_integral_comp_of_compact_quantizers
    {X : Type*} [PseudoMetricSpace X] [MeasurableSpace X] [BorelSpace X]
    {Y : Set X} (hY : IsCompact Y) {μ : Measure X} [IsFiniteMeasure μ]
    (hμ : ∀ᵐ x ∂μ, x ∈ Y) {Q : ℕ → X → X}
    (hQ : ∀ n, Measurable (Q n)) (hmem : ∀ n x, Q n x ∈ Y)
    (hlim : TendstoUniformlyOn Q id Filter.atTop Y)
    {φ : X → ℝ} (hφ : Continuous φ) :
    Filter.Tendsto (fun n => ∫ x, φ (Q n x) ∂μ) Filter.atTop
      (nhds (∫ x, φ x ∂μ)) := by
…

theorem OAI.Problem358.exists_finite_nearest_selection line 127

Source documentation

A Borel nearest-point selection on a finite set, with a default point.

theorem exists_finite_nearest_selection
    {X : Type*} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X]
    (y₀ : X) (s : Finset X) :
    ∃ q : SimpleFunc X X, (∀ x, q x = y₀ ∨ q x ∈ s) ∧
      ∀ x y, y ∈ s → dist (q x) x ≤ dist y x := by
…

theorem OAI.Problem358.exists_compact_quantizer line 172

Source documentation

Compact sets admit finite-range Borel quantizers valued in the same set.

theorem exists_compact_quantizer
    {X : Type*} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [SecondCountableTopology X]
    {Y : Set X} (hY : IsCompact Y) (hne : Y.Nonempty)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ q : SimpleFunc X X, (∀ x, q x ∈ Y) ∧ ∀ x ∈ Y, dist (q x) x < ε := by
…

theorem OAI.Problem358.quantizer_graph_cost_le line 192

Source documentation

A pointwise quantization error bounds the cost of its induced transport plan.

theorem quantizer_graph_cost_le {d : ℕ} {μ : Measure (E d)}
    [IsProbabilityMeasure μ] {Y : Set (E d)} (hμ : IsSupported μ Y)
    {ε : ℝ} (hε : 0 ≤ ε) {q : E d → E d} (hq : Measurable q)
    (herr : ∀ x ∈ Y, dist (q x) x ≤ ε) :
    quadraticPlanCost (graphPlan μ q) ≤ ENNReal.ofReal (ε ^ 2) := by
…

theorem OAI.Problem358.simpleFunc_map_finite_support line 214

Source documentation

Pushing a measure through a simple function gives a finitely supported measure.

theorem simpleFunc_map_finite_support {d : ℕ} (μ : Measure (E d))
    (q : SimpleFunc (E d) (E d)) :
    (Set.range q).Finite ∧ IsSupported (Measure.map q μ) (Set.range q) := by
…

theorem OAI.Problem358.exists_finite_target_approximation line 226

Source documentation

Finite supported approximants remain inside the original compact target.

theorem exists_finite_target_approximation {d : ℕ} {μ : Measure (E d)}
    [IsProbabilityMeasure μ] {Y : Set (E d)}
    (hY : IsCompact Y) (hne : Y.Nonempty) (hμ : IsSupported μ Y)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ q : SimpleFunc (E d) (E d),
      (∀ x, q x ∈ Y) ∧
      IsProbabilityMeasure (Measure.map q μ) ∧
      IsSupported (Measure.map q μ) Y ∧
      IsSupported (Measure.map q μ) (Set.range q) ∧
      quadraticPlanCost (graphPlan μ q) ≤ ENNReal.ofReal (ε ^ 2) := by
…

theorem OAI.Problem358.wasserstein2_map_le_quantization_error line 248

Source documentation

The problem's transport distance is controlled by a uniform quantization error.

theorem wasserstein2_map_le_quantization_error {d : ℕ} {μ : Measure (E d)}
    [IsProbabilityMeasure μ] {Y : Set (E d)} (hμ : IsSupported μ Y)
    {ε : ℝ} (hε : 0 ≤ ε) {q : E d → E d} (hq : Measurable q)
    (herr : ∀ x ∈ Y, dist (q x) x ≤ ε) :
    wasserstein2 μ (Measure.map q μ) ≤ ε := by
…

theorem OAI.Problem358.exists_finite_supported_wasserstein_approximation line 277

Source documentation

Every compactly supported probability admits finite supported probabilities arbitrarily close in the exact transport distance used by the challenge.

theorem exists_finite_supported_wasserstein_approximation {d : ℕ}
    {μ : Measure (E d)} [IsProbabilityMeasure μ] {Y : Set (E d)}
    (hY : IsCompact Y) (hne : Y.Nonempty) (hμ : IsSupported μ Y)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ (ν : Measure (E d)) (F : Set (E d)), F.Finite ∧ F ⊆ Y ∧
      IsProbabilityMeasure ν ∧ IsSupported ν F ∧ IsSupported ν Y ∧
      wasserstein2 μ ν ≤ ε := by
…

theorem OAI.Problem358.exists_positive_atomic_support line 311

Source documentation

Zero-mass sites can be discarded from any finite support without changing the measure.

theorem exists_positive_atomic_support {d : ℕ} {μ : Measure (E d)}
    [IsProbabilityMeasure μ] {F : Set (E d)} (hF : F.Finite)
    (hμ : IsSupported μ F) :
    ∃ S : Finset (E d), S.Nonempty ∧ (S : Set (E d)) ⊆ F ∧
      (∀ x ∈ S, 0 < μ {x}) ∧ (∑ x ∈ S, μ {x}) = 1 ∧
      μ = ∑ x ∈ S, μ {x} • Measure.dirac x := by
…

theorem OAI.Problem358.exists_positive_real_atomic_support line 344

Source documentation

The finite-support representation can use positive ordinary real weights.

theorem exists_positive_real_atomic_support {d : ℕ} {μ : Measure (E d)}
    [IsProbabilityMeasure μ] {F : Set (E d)} (hF : F.Finite)
    (hμ : IsSupported μ F) :
    ∃ S : Finset (E d), S.Nonempty ∧ (S : Set (E d)) ⊆ F ∧
      (∀ x ∈ S, 0 < (μ {x}).toReal) ∧ (∑ x ∈ S, (μ {x}).toReal) = 1 ∧
      μ = ∑ x ∈ S, ENNReal.ofReal ((μ {x}).toReal) • Measure.dirac x := by
…

theorem OAI.Problem358.exists_positive_finite_atomic_presentation line 360

Source documentation

A finite supported probability has a presentation by distinct sites and strictly positive real weights, indexed by a nonempty finite ordinal.

theorem exists_positive_finite_atomic_presentation {d : ℕ} {μ : Measure (E d)}
    [IsProbabilityMeasure μ] {F : Set (E d)} (hF : F.Finite)
    (hμ : IsSupported μ F) :
    ∃ n : ℕ, 0 < n ∧ ∃ (y : Fin n → E d) (w : Fin n → ℝ),
      Function.Injective y ∧ (∀ i, y i ∈ F) ∧ (∀ i, 0 < w i) ∧
      (∑ i, w i) = 1 ∧ μ = ∑ i, ENNReal.ofReal (w i) • Measure.dirac (y i) := by
…

theorem OAI.Problem358.exists_positive_atomic_wasserstein_approximation line 388

Source documentation

Compact probabilities can be approximated by positive finite atomic families without changing the allowed target set.

theorem exists_positive_atomic_wasserstein_approximation {d : ℕ}
    {μ : Measure (E d)} [IsProbabilityMeasure μ] {Y : Set (E d)}
    (hY : IsCompact Y) (hne : Y.Nonempty) (hμ : IsSupported μ Y)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ n : ℕ, 0 < n ∧ ∃ (y : Fin n → E d) (w : Fin n → ℝ),
      Function.Injective y ∧ (∀ i, y i ∈ Y) ∧ (∀ i, 0 < w i) ∧
      (∑ i, w i) = 1 ∧
      wasserstein2 μ (∑ i, ENNReal.ofReal (w i) • Measure.dirac (y i)) ≤ ε := by
…