OAI/Computability/DeterministicSum/WeightedFeatures.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Monomial formation, weighted feature sums and exact source identities.

  1. def OAI.DeterministicThreeSum.Structured.Indexed.Monomial.value line 11
  2. lemma OAI.DeterministicThreeSum.Structured.Indexed.Monomial.value_lt line 15
  3. def OAI.DeterministicThreeSum.Structured.Indexed.Monomial.step line 18
  4. def OAI.DeterministicThreeSum.Structured.Indexed.Monomial.loop line 30
  5. def OAI.DeterministicThreeSum.Structured.Indexed.Monomial.stepState line 32
  6. lemma OAI.DeterministicThreeSum.Structured.Indexed.Monomial.index_lt line 37
  7. lemma OAI.DeterministicThreeSum.Structured.Indexed.Monomial.step_correct line 42
  8. lemma OAI.DeterministicThreeSum.Structured.Indexed.Monomial.step_frame line 73
  9. theorem OAI.DeterministicThreeSum.Structured.Indexed.Monomial.loop_correct line 82
  10. lemma OAI.DeterministicThreeSum.Structured.Indexed.Monomial.value_eq_tensor line 118
  11. theorem OAI.DeterministicThreeSum.Structured.Indexed.Monomial.value_eq_monomial line 128
  12. def OAI.DeterministicThreeSum.Structured.Indexed.FeatureDot.value line 140
  13. def OAI.DeterministicThreeSum.Structured.Indexed.FeatureDot.body line 144
  14. def OAI.DeterministicThreeSum.Structured.Indexed.FeatureDot.loop line 153
  15. def OAI.DeterministicThreeSum.Structured.Indexed.FeatureDot.bodyState line 155
  16. lemma OAI.DeterministicThreeSum.Structured.Indexed.FeatureDot.body_correct line 159
  17. lemma OAI.DeterministicThreeSum.Structured.Indexed.FeatureDot.body_frame line 181
  18. theorem OAI.DeterministicThreeSum.Structured.Indexed.FeatureDot.loop_correct line 190
  19. lemma OAI.DeterministicThreeSum.Structured.Indexed.FeatureDot.value_cast line 233
  20. def OAI.DeterministicThreeSum.Structured.Indexed.GFeature.prepare line 245
  21. def OAI.DeterministicThreeSum.Structured.Indexed.GFeature.prepared line 251
  22. def OAI.DeterministicThreeSum.Structured.Indexed.GFeature.finish line 255
  23. def OAI.DeterministicThreeSum.Structured.Indexed.GFeature.finished line 261
  24. def OAI.DeterministicThreeSum.Structured.Indexed.GFeature.body line 264
  25. def OAI.DeterministicThreeSum.Structured.Indexed.GFeature.loop line 265
  26. def OAI.DeterministicThreeSum.Structured.Indexed.GFeature.value line 267
  27. lemma OAI.DeterministicThreeSum.Structured.Indexed.GFeature.prepare_correct line 271
  28. lemma OAI.DeterministicThreeSum.Structured.Indexed.GFeature.prepare_frame line 289
  29. lemma OAI.DeterministicThreeSum.Structured.Indexed.GFeature.finish_correct line 297
  30. lemma OAI.DeterministicThreeSum.Structured.Indexed.GFeature.finish_frame line 314
  31. lemma OAI.DeterministicThreeSum.Structured.Indexed.GFeature.body_correct line 318
  32. theorem OAI.DeterministicThreeSum.Structured.Indexed.GFeature.loop_correct line 359
  33. lemma OAI.DeterministicThreeSum.Structured.Indexed.GFeature.value_cast line 407
  34. theorem OAI.DeterministicThreeSum.Structured.Indexed.E_value line 420
  35. theorem OAI.DeterministicThreeSum.Structured.Indexed.G_value line 438
  36. lemma OAI.DeterministicThreeSum.Structured.Indexed.group_enumeration_sum line 449