OAI/Analysis/PathSelection/ScalarFields.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

Regular scalar evaluation fields and germ polynomials.

  1. structure OAI.DegeneratingTrees.ScalarEvaluation line 16
  2. lemma OAI.DegeneratingTrees.ScalarEvaluation.zero line 26
  3. lemma OAI.DegeneratingTrees.ScalarEvaluation.one line 27
  4. def OAI.DegeneratingTrees.ScalarEvaluation.toGermHom line 30
  5. lemma OAI.DegeneratingTrees.ScalarEvaluation.faithful line 37
  6. lemma OAI.DegeneratingTrees.ScalarEvaluation.nonzero line 42
  7. lemma OAI.DegeneratingTrees.ScalarEvaluation.neg line 47
  8. lemma OAI.DegeneratingTrees.ScalarEvaluation.sub line 52
  9. lemma OAI.DegeneratingTrees.ScalarEvaluation.inv line 56
  10. lemma OAI.DegeneratingTrees.ScalarEvaluation.div line 65
  11. lemma OAI.DegeneratingTrees.ScalarEvaluation.pow line 69
  12. lemma OAI.DegeneratingTrees.ScalarEvaluation.sum line 76
  13. def OAI.DegeneratingTrees.ScalarEvaluation.HasScalarLimits line 87
  14. def OAI.DegeneratingTrees.ScalarEvaluation.HasDivisibleSizes line 93
  15. def OAI.DegeneratingTrees.ScalarEvaluation.HolomorphicallyClosed line 100
  16. lemma OAI.DegeneratingTrees.ScalarEvaluation.tendsto_mul line 106
  17. lemma OAI.DegeneratingTrees.ScalarEvaluation.tendsto_pow line 111
  18. lemma OAI.DegeneratingTrees.ScalarEvaluation.tendsto_div line 115
  19. lemma OAI.DegeneratingTrees.ScalarEvaluation.tendsto_inv_of_norm_atTop line 120
  20. def OAI.DegeneratingTrees.ScalarEvaluation.BoundedRatio line 128
  21. lemma OAI.DegeneratingTrees.ScalarEvaluation.boundedRatio_refl line 130
  22. lemma OAI.DegeneratingTrees.ScalarEvaluation.boundedRatio_trans line 136
  23. lemma OAI.DegeneratingTrees.ScalarEvaluation.boundedRatio_total line 145
  24. lemma OAI.DegeneratingTrees.ScalarEvaluation.exists_max_scale line 153
  25. lemma OAI.DegeneratingTrees.ScalarEvaluation.exists_root_size line 182
  26. lemma OAI.DegeneratingTrees.ScalarEvaluation.normalize_finite_coefficients line 207
  27. def OAI.DegeneratingTrees.Clock.clockSubring line 257
  28. abbrev OAI.DegeneratingTrees.Clock.ClockField line 271
  29. def OAI.DegeneratingTrees.Clock.ClockField.ofFunction line 273
  30. def OAI.DegeneratingTrees.Clock.ClockField.value line 276
  31. lemma OAI.DegeneratingTrees.Clock.ClockField.value_mem line 279
  32. lemma OAI.DegeneratingTrees.Clock.ClockField.value_eq line 282
  33. lemma OAI.DegeneratingTrees.Clock.ClockField.ofFunction_value line 285
  34. lemma OAI.DegeneratingTrees.Clock.ClockField.value_zero_iff line 289
  35. lemma OAI.DegeneratingTrees.Clock.clockField_unit_or_zero line 295
  36. instance OAI.DegeneratingTrees.Clock.clockField line 309
  37. def OAI.DegeneratingTrees.Clock.clockConstHom line 312
  38. instance OAI.DegeneratingTrees.Clock.clockAlgebra line 319
  39. def OAI.DegeneratingTrees.Clock.clockEvaluation line 322
  40. lemma OAI.DegeneratingTrees.Clock.clockEvaluation_divisible line 339
  41. lemma OAI.DegeneratingTrees.Clock.clockEvaluation_holomorphic line 355
  42. def OAI.DegeneratingTrees.ScalarEvaluation.coefficientGermHom line 375
  43. def OAI.DegeneratingTrees.ScalarEvaluation.toPolynomialGermHom line 394
  44. def OAI.DegeneratingTrees.ScalarEvaluation.polynomialValue line 397
  45. lemma OAI.DegeneratingTrees.ScalarEvaluation.polynomialValue_coeff line 400
  46. lemma OAI.DegeneratingTrees.ScalarEvaluation.polynomialValue_coeff_eventually line 405
  47. lemma OAI.DegeneratingTrees.ScalarEvaluation.polynomialValue_germ line 415
  48. lemma OAI.DegeneratingTrees.ScalarEvaluation.polynomialValue_zero line 431
  49. lemma OAI.DegeneratingTrees.ScalarEvaluation.polynomialValue_add line 435
  50. lemma OAI.DegeneratingTrees.ScalarEvaluation.polynomialValue_mul line 442
  51. lemma OAI.DegeneratingTrees.ScalarEvaluation.polynomialValue_faithful line 449
  52. lemma OAI.DegeneratingTrees.ScalarEvaluation.polynomialValue_natDegree_le line 456
  53. lemma OAI.DegeneratingTrees.ScalarEvaluation.polynomialValue_monic line 466
  54. lemma OAI.DegeneratingTrees.ScalarEvaluation.polynomial_dvd_of_eventually line 476