OAI/Algebra/FiniteTensor/JetSolutions.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Exact tensor models reconstructed from jet solutions and their algebraicity.

  1. structure OAI.PD4Tensor.Spreading.JetSolution line 22
  2. def OAI.PD4Tensor.Spreading.originalJetSolution line 34
  3. def OAI.PD4Tensor.Spreading.JetSolution.H line 47
  4. def OAI.PD4Tensor.Spreading.JetSolution.G line 51
  5. def OAI.PD4Tensor.Spreading.JetSolution.L line 54
  6. def OAI.PD4Tensor.Spreading.JetSolution.R line 59
  7. theorem OAI.PD4Tensor.Spreading.JetSolution.left_hasSubst line 62
  8. theorem OAI.PD4Tensor.Spreading.JetSolution.right_hasSubst line 65
  9. theorem OAI.PD4Tensor.Spreading.JetSolution.H_box line 68
  10. theorem OAI.PD4Tensor.Spreading.JetSolution.L_box line 74
  11. theorem OAI.PD4Tensor.Spreading.JetSolution.G_eq line 80
  12. theorem OAI.PD4Tensor.Spreading.JetSolution.R_eq line 84
  13. theorem OAI.PD4Tensor.Spreading.JetSolution.H_constant line 88
  14. theorem OAI.PD4Tensor.Spreading.JetSolution.H_first line 96
  15. theorem OAI.PD4Tensor.Spreading.JetSolution.G_constant line 107
  16. theorem OAI.PD4Tensor.Spreading.JetSolution.G_first line 111
  17. theorem OAI.PD4Tensor.Spreading.JetSolution.comp_left line 119
  18. theorem OAI.PD4Tensor.Spreading.JetSolution.comp_right line 126
  19. theorem OAI.PD4Tensor.Spreading.JetSolution.left_vanishing line 132
  20. theorem OAI.PD4Tensor.Spreading.JetSolution.right_vanishing line 141
  21. theorem OAI.PD4Tensor.Spreading.JetSolution.left_identity line 147
  22. theorem OAI.PD4Tensor.Spreading.JetSolution.right_identity line 163
  23. def OAI.PD4Tensor.Spreading.JetSolution.model line 178
  24. def OAI.PD4Tensor.Spreading.JetSolution.primitives line 203
  25. structure OAI.PD4Tensor.Spreading.JetSolution.Algebraic line 221
  26. theorem OAI.PD4Tensor.Spreading.constant_series_algebraic line 225
  27. theorem OAI.PD4Tensor.Spreading.JetSolution.algebraicData line 231
  28. theorem OAI.PD4Tensor.Spreading.no_algebraic_jet_solution line 258
  29. def OAI.PD4Tensor.Spreading.TensorAlgebraicApproximation line 266