`Learning.randomSampling.action_tendsto_any`🔗

Theorem

The minimum distance from sampled actions to any point tends to zero.

Types

𝓐 : Type u_1m𝓐 : MeasurableSpace 𝓐A measurable space is a space equipped with a σ-algebra.PseudoMetricSpace 𝓐A pseudometric space is a type endowed with a ℝ-valued distance dist satisfying reflexivity dist x x = 0, commutativity dist x y = dist y x, and the triangle inequality dist x z ≤ dist x y +…SecondCountableTopology 𝓐A second-countable space is one with a countable basis.OpensMeasurableSpace 𝓐A space with MeasurableSpace and TopologicalSpace structures such that all open sets are measurable.
𝓨 : Type u_2m𝓨 : MeasurableSpace 𝓨
Ω : Type u_3mΩ : MeasurableSpace Ω

Given

μ : MeasureTheory.Measure 𝓐A measure is defined to be an outer measure that is countably additive on measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure.MeasureTheory.IsProbabilityMeasure μA measure μ is called a probability measure if μ univ = 1.μ.IsOpenPosMeasureA measure is said to be IsOpenPosMeasure if it is positive on nonempty open sets.
P : MeasureTheory.Measure ΩMeasureTheory.IsProbabilityMeasure P
A : ℕ → Ω → 𝓐
Y : ℕ → Ω → 𝓨
f : 𝓐 → 𝓨
a : 𝓐
ε : ℝ

Assuming

hf : Measurable fimplicitA function f between measurable spaces is measurable if the preimage of every measurable set is measurable.
h : IsAlgEnvSeq A Y (randomSampling μ) (evalEnv f hf) PAn algorithm-environment sequence: a sequence of actions and feedbacks generated by an algorithm interacting with an environment.
hε : 0 < ε

Then

Filter.Tendsto (fun i => P {x | ε ≤ Function.min fun j => dist (A (↑j) x) a}) Filter.atTop (nhds 0)

Filter.Tendsto is the generic "limit of a function" predicate.

MeasurableSpace : Type u_6 → Type u_6

A measurable space is a space equipped with a σ-algebra.

PseudoMetricSpace : Type u → Type u

A pseudometric space is a type endowed with a `ℝ`-valued distance `dist` satisfying
reflexivity `dist x x = 0`, commutativity `dist x y = dist y x`, and the triangle inequality
`dist x z ≤ dist x y + dist y z`.

Note that we do not require `dist x y = 0 → x = y`. See metric spaces (`MetricSpace`) for the
similar class with that stronger assumption.

Any pseudometric space is a topological space and a uniform space (see `TopologicalSpace`,
`UniformSpace`), where the topology and uniformity come from the metric.
Note that a T1 pseudometric space is just a metric space.

We make the uniformity/topology part of the data instead of deriving it from the metric. This e.g.
ensures that we do not get a diamond when doing
`[PseudoMetricSpace α] [PseudoMetricSpace β] : TopologicalSpace (α × β)`:
The product metric and product topology agree, but not definitionally so.
See Note [forgetful inheritance].

SecondCountableTopology : (α : Type u) → [t : TopologicalSpace α] → Prop

A second-countable space is one with a countable basis.

OpensMeasurableSpace : (α : Type u_6) → [TopologicalSpace α] → [h : MeasurableSpace α] → Prop

A space with `MeasurableSpace` and `TopologicalSpace` structures such that
all open sets are measurable.

MeasureTheory.IsProbabilityMeasure : {α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → Prop

A measure `μ` is called a probability measure if `μ univ = 1`.

MeasureTheory.Measure.IsOpenPosMeasure : {X : Type u_1} → [TopologicalSpace X] → {m : MeasurableSpace X} → MeasureTheory.Measure X → Prop

A measure is said to be `IsOpenPosMeasure` if it is positive on nonempty open sets.

MeasureTheory.Measure : (α : Type u_5) → [MeasurableSpace α] → Type u_5

A measure is defined to be an outer measure that is countably additive on
measurable sets, with the additional assumption that the outer measure is the canonical
extension of the restricted measure.

The measure of a set `s`, denoted `μ s`, is an extended nonnegative real. The real-valued version
is written `μ.real s`.

Nat : Type

The natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.

Real : Type

The type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
numbers.

Measurable : {α : Type u_1} → {β : Type u_2} → [MeasurableSpace α] → [MeasurableSpace β] → (α → β) → Prop

A function `f` between measurable spaces is measurable if the preimage of every
measurable set is measurable.

Learning.IsAlgEnvSeq : {𝓐 : Type u_1} →
  {𝓨 : Type u_2} →
    {Ω : Type u_3} →
      {m𝓐 : MeasurableSpace 𝓐} →
        {m𝓨 : MeasurableSpace 𝓨} →
          {mΩ : MeasurableSpace Ω} →
            (ℕ → Ω → 𝓐) →
              (ℕ → Ω → 𝓨) →
                Learning.Algorithm 𝓐 𝓨 →
                  Learning.Environment 𝓐 𝓨 → (P : MeasureTheory.Measure Ω) → [MeasureTheory.IsFiniteMeasure P] → Prop

An algorithm-environment sequence: a sequence of actions and feedbacks generated
by an algorithm interacting with an environment.

Go to its page

Learning.randomSampling : {𝓐 : Type u_1} →
  {𝓨 : Type u_2} →
    {m𝓐 : MeasurableSpace 𝓐} →
      {m𝓨 : MeasurableSpace 𝓨} →
        (μ : MeasureTheory.Measure 𝓐) → [MeasureTheory.IsProbabilityMeasure μ] → Learning.Algorithm 𝓐 𝓨

The _Random Sampling_ algorithm, which samples from a fixed probability
measure at each iteration.

Go to its page

Learning.evalEnv : {𝓐 : Type u_1} →
  {𝓨 : Type u_2} →
    {m𝓐 : MeasurableSpace 𝓐} → {m𝓨 : MeasurableSpace 𝓨} → (f : 𝓐 → 𝓨) → Measurable f → Learning.Environment 𝓐 𝓨

The evaluation environment where the feedback is given by evaluating a fixed measurable function
`f` at the chosen action.

Go to its page

LT.lt : {α : Type u} → [self : LT α] → α → α → Prop

The less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`.

Filter.Tendsto : {α : Type u_1} → {β : Type u_2} → (α → β) → Filter α → Filter β → Prop

`Filter.Tendsto` is the generic "limit of a function" predicate.
`Tendsto f l₁ l₂` asserts that for every `l₂` neighborhood `a`,
the `f`-preimage of `a` is an `l₁` neighborhood.

Set.ofPred : {α : Type u} → (α → Prop) → Set α

Turn a predicate `p : α → Prop` into a set, also written as `{x | p x}`

LE.le : {α : Type u} → [self : LE α] → α → α → Prop

The less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`.

Function.min : {ι : Type u_1} → {α : Type u_2} → [LinearOrder α] → [Fintype ι] → [Nonempty ι] → (ι → α) → α

The minimum value of a tuple.

Go to its page

Dist.dist : {α : Type u_3} → [self : Dist α] → α → α → ℝ

Distance between two points

Filter.atTop : {α : Type u_2} → [Preorder α] → Filter α

`atTop` is the filter representing the limit `→ ∞` on an ordered set.
It is generated by the collection of up-sets `{b | a ≤ b}`.
(The preorder need not have a top element for this to be well defined,
and indeed is trivial when a top element `x` exists, i.e., it coincides with `pure x`.)

nhds : {X : Type u_3} → [TopologicalSpace X] → X → Filter X

A set is called a neighborhood of `x` if it contains an open set around `x`. The set of all
neighborhoods of `x` forms a filter, the neighborhood filter at `x`, is here defined as the
infimum over the principal filters of all open sets containing `x`.

Code

theorem action_tendsto_any (h : IsAlgEnvSeq A Y (randomSampling μ) (evalEnv f hf) P) (a : 𝓐)
    {ε : ℝ} (hε : 0 < ε) :
    Tendsto (fun i => P {x | ε ≤ (fun (j : Iic i) ↦ dist (A j.1 x) a).min}) atTop (𝓝 0)

Proof

by
  set randomSampling_alg := randomSampling (𝓨 := 𝓨) μ
  refine tendsto_zero_of_le (g := fun n ↦ P (⋂ i ∈ Iic n, {x | ε ≤ dist (A i x) a})) ?_ ?_
  · have inter_prod (n : ℕ) : P (⋂ j ∈ Iic n, {x | ε ≤ dist (A j x) a}) =
        ∏ j ∈ Iic n, P {x | ε ≤ dist (A j x) a} := by
      refine iIndepSet.meas_biInter ?_ _
      rw [iIndepSet_iff_meas_biInter fun i ↦ ?_]
      · intro s
        have iIndep_actions := randomSampling.iIndep_action h
        rw [iIndepFun_iff_measure_inter_preimage_eq_mul] at iIndep_actions
        have meas_dist : ∀ i ∈ s, MeasurableSet {x | ε ≤ dist x a} := by
          intro i hs
          measurability
        specialize iIndep_actions s meas_dist
        simpa [Set.preimage] using iIndep_actions
      · have hAi := h.measurable_action i
        measurability
    simp_rw [inter_prod]
    have prod_law (n : ℕ) : ∏ j ∈ Iic n, P {x | ε ≤ dist (A j x) a} =
        ∏ j ∈ Iic n, μ {x | ε ≤ dist x a} := by
      refine prod_congr rfl fun j hj ↦ ?_
      have hlaw (n : ℕ) : HasLaw (A n) μ P := randomSampling.hasLaw_action h n
      rw [← (hlaw j).map_eq, P.map_apply]
      · simp
      · exact h.measurable_action j
      · measurability
    simp_rw [prod_law]
    simp only [prod_const, Nat.card_Iic]
    refine tendsto_pow_atTop_nhds_zero_of_lt_one ?_ |> Tendsto.comp <| tendsto_add_atTop_nat 1
    have compl : {x | ε ≤ dist x a} = {x | dist x a < ε}ᶜ := by
      ext a
      simp
    rw [compl, measure_compl (by measurability) (by simp), measure_univ]
    refine ENNReal.sub_lt_self (by simp) (by simp) ?_
    exact (Metric.measure_ball_pos μ a hε).ne'
  · intro n
    refine measure_mono ?_
    simp only [mem_Iic, Set.subset_iInter_iff, Set.ofPred_subset_ofPred]
    intro i hi ω (hω : ε ≤ (fun (j : Iic n) ↦ dist (A j.1 ω) a).min)
    simp_all only [univ_eq_attach, le_inf'_iff, mem_attach, forall_const, Subtype.forall, mem_Iic]

Actions: Source · Open Issue

Meaning last changed in v4.34.0-rc2-39-gb743f31 (2026-09-08), the 5th recorded change.

Self-contained, with its dependencies inlined and proofs replaced by sorry: download the raw file · open it in the Lean web editor.

Dependency graph

Audit surface: 10 project declarations, 87 external constants

✓ Proved: no sorry anywhere in its closure

This is the tool's own reading of one build's recorded axioms, and it is not robust against an author who wants it to pass. Checking meant to be relied on should go through Comparator, which replays the proof through the kernel from an export against an explicit list of permitted axioms.

Learning.randomSampling.action_tendsto_any🔗

`Learning.randomSampling.action_tendsto_any`🔗