CoordinateEmbedding.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem326.Affine.embedCoordinates line 14
Source documentation
Extend coordinates along an injection, using the constant baseline on its complement.
```
def embedCoordinates {k d : ℕ} (e : Fin k ↪ Fin d) (t : ℝ)
    (s : Fin k → ℝ) : Fin d → ℝ :=
…
```
theorem OAI.Problem326.Affine.embedCoordinates_apply line 18
theorem OAI.Problem326.Affine.embedCoordinates_outside line 25
def OAI.Problem326.Affine.Label.embed line 33
Source documentation
The larger-dimensional label used for a fixed-minimum type.
```
def Label.embed {k d : ℕ} (e : Fin k ↪ Fin d) (t β : ℝ)
    (L : Label k) : Label d where
…
```
Mentions: OAI.Problem326.Affine.Label
theorem OAI.Problem326.Affine.embedCoordinates_dot line 38

theorem OAI.Problem326.Affine.Label.embed_value line 56

Source documentation

Embedded affine values differ from their projected values by a common term.

theorem Label.embed_value {k d : ℕ} (e : Fin k ↪ Fin d) (t β h : ℝ)
    (L : Label k) (x : Fin d → ℝ) :
    (L.embed e t β).value h x = L.value h (fun j => x (e j)) +
      t * ((∑ i, x i) - ∑ j, x (e j)) - h ^ β := by
…

Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.Label.value

theorem OAI.Problem326.Affine.Label.embed_injective line 64

theorem OAI.Problem326.Affine.active_embed_iff line 83

Source documentation

Common baseline and offset terms preserve all comparisons, including ties.

theorem active_embed_iff {k d : ℕ} (e : Fin k ↪ Fin d) (t β h : ℝ)
    (Λ : Finset (Label k)) (L : Label k) (x : Fin d → ℝ) :
    Active (Λ.image (Label.embed e t β)) (L.embed e t β) h x ↔
      Active Λ L h (fun j => x (e j)) := by
…

Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.Active, OAI.Problem326.Affine.Label.embed

theorem OAI.Problem326.Affine.cube_embedCoordinates line 106
theorem OAI.Problem326.Affine.hasMinimum_embedCoordinates line 118
theorem OAI.Problem326.Affine.embedCoordinates_gt_baseline_iff line 139
Source documentation
The raised coordinates of the embedded slope are exactly the injected coordinates.
```
theorem embedCoordinates_gt_baseline_iff {k d : ℕ} (e : Fin k ↪ Fin d)
    {t : ℝ} {s : Fin k → ℝ} (hs : ∀ j, t < s j) (i : Fin d) :
    t < embedCoordinates e t s i ↔ i ∈ Set.range e := by
…
```
Mentions: OAI.Problem326.Affine.embedCoordinates
theorem OAI.Problem326.Affine.tendsto_project_coordinates line 148
theorem OAI.Problem326.Affine.powerPoint_project line 154

theorem OAI.Problem326.Affine.active_project_of_active line 159

Source documentation

Activity in any larger family restricts to the projected lower-dimensional family.

theorem active_project_of_active {k d : ℕ} (e : Fin k ↪ Fin d) (t β h : ℝ)
    {Λ : Finset (Label k)} {Γ : Finset (Label d)} {L : Label k}
    (hΛ : Λ.image (Label.embed e t β) ⊆ Γ) (hL : L ∈ Λ)
    (p : Fin d → ℝ)
    (ha : Active Γ (L.embed e t β) h (powerPoint h p)) :
    Active Λ L h (powerPoint h (fun j => p (e j))) := by
…

Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.Label.embed, OAI.Problem326.Affine.Active, OAI.Problem326.Affine.powerPoint

theorem OAI.Problem326.Affine.embedded_error_on_range line 170

Source documentation

A projected norm estimate controls every raised coordinate of the larger slope.

theorem embedded_error_on_range {k d : ℕ} (e : Fin k ↪ Fin d)
    (t : ℝ) {s : Fin k → ℝ} {p : Fin d → ℝ} {ε : ℝ}
    (herr : ‖(fun j => p (e j)) - s‖ < ε) :
    ∀ i ∈ Set.range e, |p i - embedCoordinates e t s i| < ε := by
…

Mentions: OAI.Problem326.Affine.embedCoordinates

def OAI.Problem326.Affine.supportEmbedding line 181
Source documentation
Canonical coordinate injection for a finite support, built from its finite enumeration.
```
def supportEmbedding {d : ℕ} (U : Finset (Fin d)) : Fin U.card ↪ Fin d :=
…
```
theorem OAI.Problem326.Affine.supportEmbedding_mem line 184
theorem OAI.Problem326.Affine.range_supportEmbedding line 188

theorem OAI.Problem326.Affine.embedded_family_data line 199

Source documentation

Every member of an embedded nonempty family has the required baseline minimum.

theorem embedded_family_data {k d : ℕ} (e : Fin k ↪ Fin d)
    (hkd : k < d) {a t β b : ℝ}
    (hat : a ≤ t) (htβ : t < β) (hβb : β < b)
    (Λ : Finset (Label k)) (hne : Λ.Nonempty)
    (hslopes : ∀ L ∈ Λ, Cube β b L.slope) :
    (Λ.image (Label.embed e t β)).Nonempty ∧
      ∀ J ∈ Λ.image (Label.embed e t β),
        Cube a b J.slope ∧ HasMinimum J.slope t ∧
        ∀ i, t < J.slope i ↔ i ∈ Set.range e := by
…

Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.Cube, OAI.Problem326.Affine.Label.embed, OAI.Problem326.Affine.HasMinimum