Documentation

LeanPool.NandakumarRamanaRao.NRR.EMP.VariableBody.WeightBox

NRR.EMP.VariableBody.WeightBox — a compact codomain for bounded weights #

For a fixed arity n and a real bound M, the weight box is the subtype of weight vectors whose coordinates are all bounded in absolute value by M:

WeightBox n M = {w : Fin n → ℝ // ∀ i, |w i| ≤ M}

Carrying the inherited subtype topology, the box is a compact Hausdorff space for every real M; when M < 0 it is empty, which is still compact. Identifying the defining condition with a finite product of closed intervals Set.Icc (-M) M gives compactness from finite-product compactness of the intervals (each interval is compact even when it is empty).

This compact box is the intended codomain for the equal-area weight selection, whose closed graph together with uniqueness will yield continuity of the selection.

source
@[reducible, inline]
abbrev NRR.EMP.VariableBody.WeightBox (n : ℕ) (M : ℝ) :
Type

The weight box: weight vectors of arity n whose coordinates are bounded by M in absolute value. It is realized as an abbrev over a subtype so that the subtype topology and Hausdorff structure are inherited automatically (no TopologicalSpace instance is redeclared).

Equations
Instances For
    source
    theorem NRR.EMP.VariableBody.WeightBox.setOf_eq_pi {n : ℕ} {M : ℝ} :
    {w : Fin n → ℝ | ∀ (i : Fin n), |w i| ≤ M} = Set.univ.pi fun (x : Fin n) => Set.Icc (-M) M

    The defining condition of the weight box, phrased as membership in a finite product of the closed interval Set.Icc (-M) M.

    source
    theorem NRR.EMP.VariableBody.WeightBox.isCompact_setOf {n : ℕ} {M : ℝ} :
    IsCompact {w : Fin n → ℝ | ∀ (i : Fin n), |w i| ≤ M}

    The defining set of the weight box is compact, being a finite product of compact intervals.

    source
    instance NRR.EMP.VariableBody.WeightBox.instCompactSpace {n : ℕ} {M : ℝ} :
    CompactSpace (WeightBox n M)

    The weight box is a compact space for every real M; when M < 0 it is empty but still compact.

    source
    def NRR.EMP.VariableBody.WeightBox.valContinuous (n : ℕ) (M : ℝ) :
    C(WeightBox n M, Fin n → ℝ)

    The coordinate projection of the weight box as a bundled continuous map.

    Equations
    Instances For
      source
      @[simp]
      theorem NRR.EMP.VariableBody.WeightBox.valContinuous_apply {n : ℕ} {M : ℝ} (w : WeightBox n M) :
      (valContinuous n M) w = ↑w
      source
      theorem NRR.EMP.VariableBody.WeightBox.range_val {n : ℕ} {M : ℝ} :
      (Set.range fun (w : WeightBox n M) => ↑w) = {w : Fin n → ℝ | ∀ (i : Fin n), |w i| ≤ M}

      The range of the coordinate projection is exactly the defining set of the weight box.

      source
      theorem NRR.EMP.VariableBody.WeightBox.isClosed_range {n : ℕ} {M : ℝ} :
      IsClosed (Set.range fun (w : WeightBox n M) => ↑w)

      The range of the coordinate projection is closed (it is a finite product of closed intervals).

      source
      theorem NRR.EMP.VariableBody.WeightBox.ext {n : ℕ} {M : ℝ} {u v : WeightBox n M} (h : ↑u = ↑v) :
      u = v

      Extensionality for the weight box: elements are equal when their coordinate vectors agree.

      source
      theorem NRR.EMP.VariableBody.WeightBox.ext_iff {n : ℕ} {M : ℝ} {u v : WeightBox n M} :
      u = v ↔ ↑u = ↑v