OAI/Analysis/MassAction/TypeFamily.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem326.Affine.typeFamily line 15

   Source documentation

   The type-k family is the finite union over coordinate injections. Indexing by all injections avoids dependent coordinate casts; every k-element support is represented.

   def typeFamily {k d : ℕ} (t β : ℝ)
       (Λ : (Fin k ↪ Fin d) → Finset (Label k)) : Finset (Label d) :=
   …

   Mentions: OAI.Problem326.Affine.Label

2. theorem OAI.Problem326.Affine.mem_typeFamily line 19
3. theorem OAI.Problem326.Affine.embeddedFamily_subset_typeFamily line 27
4. theorem OAI.Problem326.Affine.typeFamily_nonempty line 34
5. theorem OAI.Problem326.Affine.typeFamily_member_data line 42

   Source documentation

   Every member of a type family has baseline minimum and exactly the injected raised support.

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

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

6. theorem OAI.Problem326.Affine.typeFamily_support_exists line 55

   Source documentation

   Every prescribed support of size k occurs in the type family.

   theorem typeFamily_support_exists {k d : ℕ} {t β b : ℝ} (htβ : t < β)
       (Λ : (Fin k ↪ Fin d) → Finset (Label k))
       (hne : ∀ e, (Λ e).Nonempty)
       (hslopes : ∀ e L, L ∈ Λ e → Cube β b L.slope)
       (U : Finset (Fin d)) (hU : U.card = k) :
       ∃ J ∈ typeFamily t β Λ, ∀ i, t < J.slope i ↔ i ∈ U := by
   …

   Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.Cube, OAI.Problem326.Affine.typeFamily

7. theorem OAI.Problem326.Affine.typeFamily_active_project line 72

   Source documentation

   All comparisons in the total type family imply the lower-dimensional activity hypothesis.

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

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

8. theorem OAI.Problem326.Affine.typeFamily_support_data line 81

   Source documentation

   The support data in finite-set form, matching the layer-certificate interface.

   theorem typeFamily_support_data {k d : ℕ} (t β : ℝ)
       (Λ : (Fin k ↪ Fin d) → Finset (Label k)) {b : ℝ}
       (hslopes : ∀ e L, L ∈ Λ e → Cube β b L.slope)
       {J : Label d} (hJ : J ∈ typeFamily t β Λ) :
       ∃ U : Finset (Fin d), U.card = k ∧
         (∀ i ∈ U, β ≤ J.slope i ∧ J.slope i ≤ b) ∧
         (∀ i ∉ U, J.slope i = t) := by
   …

   Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.Cube, OAI.Problem326.Affine.typeFamily

9. theorem OAI.Problem326.Affine.typeFamily_supported_competitor line 100

   Source documentation

   Every support has a competitor equal to the baseline off that support.

   theorem typeFamily_supported_competitor {k d : ℕ} (t β : ℝ)
       (Λ : (Fin k ↪ Fin d) → Finset (Label k))
       (hne : ∀ e, (Λ e).Nonempty)
       (U : Finset (Fin d)) (hU : U.card = k) :
       ∃ J ∈ typeFamily t β Λ, ∀ i ∉ U, J.slope i = t := by
   …

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

10. theorem OAI.Problem326.Affine.Label.embed_normalized_offset line 116

    Source documentation

    A lower-dimensional little-offset quotient becomes the normalized -1 offset required of a positive type.

    theorem Label.embed_normalized_offset {k d : ℕ} (e : Fin k ↪ Fin d)
        (t β : ℝ) (L : Label k)
        (hL : Tendsto (fun h : ℝ => L.offset h / h ^ β) (𝓝[>] 0) (𝓝 0)) :
        Tendsto (fun h : ℝ => (L.embed e t β).offset h / h ^ β)
          (𝓝[>] 0) (𝓝 (-1)) := by
    …

    Mentions: OAI.Problem326.Affine.Label