OAI/Analysis/DiamondDistortion/StartBounds.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.DiamondDistortion.StartModel.repComplete line 19
  2. def OAI.DiamondDistortion.StartModel.outputCoordinate line 26
  3. def OAI.DiamondDistortion.StartModel.outputContinuous line 31
  4. instance OAI.DiamondDistortion.StartModel.kernelClosed line 33
  5. abbrev OAI.DiamondDistortion.StartModel.FullComponent line 38

    Source documentation

    The complete infimal-cost space of all finite-cost coordinate outputs, modulo representations with zero output.

    abbrev FullComponent (h : ℕ) := Rep h ⧸ LinearMap.ker (output h)

    Mentions: OAI.DiamondDistortion.StartModel.Rep, OAI.DiamondDistortion.StartModel.output

  6. instance OAI.DiamondDistortion.StartModel.fullComponentNormed line 39
  7. instance OAI.DiamondDistortion.StartModel.fullComponentNormedSucc line 43

    Source comment

    Help typeclass matching across the recursive successor representation model.
    instance fullComponentNormedSucc (h : ℕ) : NormedAddCommGroup (FullComponent (h+1)) := fullComponentNormed (h+1)

    Mentions: OAI.DiamondDistortion.StartModel.FullComponent, OAI.DiamondDistortion.StartModel.fullComponentNormed

  8. instance OAI.DiamondDistortion.StartModel.fullComponentComplete line 44
  9. def OAI.DiamondDistortion.StartModel.componentEmbedding line 45
  10. lemma OAI.DiamondDistortion.StartModel.componentEmbedding_norm line 47
  11. def OAI.DiamondDistortion.StartModel.finiteOutputs line 50

    Source documentation

    The dense class of representations whose coordinate output is finite.

    def finiteOutputs (h : ℕ) : Submodule ℝ (Rep h) :=
…

    Mentions: OAI.DiamondDistortion.StartModel.Rep

  12. def OAI.DiamondDistortion.StartModel.rootInjection line 53
  13. def OAI.DiamondDistortion.StartModel.childrenInjection line 56
  14. def OAI.DiamondDistortion.StartModel.childInjection line 59
  15. lemma OAI.DiamondDistortion.StartModel.output_rootInjection line 61
  16. lemma OAI.DiamondDistortion.StartModel.rootInjection_finite line 68
  17. lemma OAI.DiamondDistortion.StartModel.childInjection_finite line 81
  18. lemma OAI.DiamondDistortion.StartModel.finiteOutputs_dense line 110
  19. lemma OAI.DiamondDistortion.StartModel.componentEmbedding_dense line 143
  20. abbrev OAI.DiamondDistortion.StartModel.FullSpace line 157

    Source documentation

    All countable finite-cost start outputs, componentwise quotient, outer ℓ².

    abbrev FullSpace := lp (fun h : ℕ => FullComponent (h+1)) 2

    Mentions: OAI.DiamondDistortion.StartModel.FullComponent

  21. def OAI.DiamondDistortion.StartModel.fullEmbedding line 158
  22. lemma OAI.DiamondDistortion.StartModel.fullEmbedding_norm line 160
  23. lemma OAI.DiamondDistortion.StartModel.fullEmbedding_dense line 162
  24. def OAI.DiamondDistortion.StartModel.fullEquiv line 164
  25. lemma OAI.DiamondDistortion.StartModel.fullEquiv_embedding line 165
  26. def OAI.DiamondDistortion.StartModel.fullHeads line 167
  27. theorem OAI.DiamondDistortion.StartModel.full_graph line 169
  28. def OAI.DiamondDistortion.PathModel.linearFullHeads line 176
  29. def OAI.DiamondDistortion.PathModel.quadraticFullHeads line 177
  30. theorem OAI.DiamondDistortion.PathModel.linear_full_flow_graph line 179
  31. theorem OAI.DiamondDistortion.PathModel.linear_full_trimming_graph line 183
  32. theorem OAI.DiamondDistortion.PathModel.linear_full_clipping_graph line 186
  33. theorem OAI.DiamondDistortion.PathModel.linear_full_vanishing_graph line 190
  34. theorem OAI.DiamondDistortion.PathModel.quadratic_full_graph line 193
  35. theorem OAI.DiamondDistortion.PathModel.stopped_full_graph line 197
  36. theorem OAI.DiamondDistortion.PathModel.quadratic_full_component_graph line 201
  37. theorem OAI.DiamondDistortion.PathModel.quadratic_full_relative_graph line 206
  38. theorem OAI.DiamondDistortion.PathModel.quadratic_full_tail_seven_graph line 210
  39. theorem OAI.DiamondDistortion.PathModel.quadratic_full_pruning_graph line 214
  40. lemma OAI.DiamondDistortion.Diamond.UnitLensBound.mono_separation line 225

    Source documentation

    A larger separation can use the same unit-lens bound.

    lemma UnitLensBound.mono_separation {X : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X] {ε ε' ρ : ℝ} (h : UnitLensBound X ε ρ)
    (hε : ε ≤ ε') : UnitLensBound X ε' ρ :=
…

    Mentions: OAI.DiamondDistortion.Diamond.UnitLensBound

  41. lemma OAI.DiamondDistortion.Diamond.QuadraticLens.positive_gap line 229