OAI/Analysis/SegmentLenses/Basic.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Segment tests, their completion, and coordinate functionals

  1. abbrev OAI.SegmentLenses.InfiniteVertex line 30

    Also declared: ComparatorChallenges/MidpointLenses.lean:18 (same declaration text).

  2. def OAI.SegmentLenses.ForestVertex line 34

    Also declared: ComparatorChallenges/MidpointLenses.lean:20 (same declaration text).

  3. def OAI.SegmentLenses.ForestAncestor line 37

    Also declared: ComparatorChallenges/MidpointLenses.lean:22 (same declaration text).

  4. def OAI.SegmentLenses.IsInterval line 41

    Also declared: ComparatorChallenges/MidpointLenses.lean:25 (same declaration text).

  5. def OAI.SegmentLenses.Ancestral line 45

    Also declared: ComparatorChallenges/MidpointLenses.lean:28 (same declaration text).

  6. class OAI.SegmentLenses.SegmentSystem line 49

    Also declared: ComparatorChallenges/MidpointLenses.lean:31 (same declaration text).

  7. structure OAI.SegmentLenses.SegmentFamily line 55

    Also declared: ComparatorChallenges/MidpointLenses.lean:35 (same declaration text).

  8. instance OAI.SegmentLenses.SegmentFamily.(instance at line 63) line 63
  9. def OAI.SegmentLenses.SegmentFamily.column line 66

    Also declared: ComparatorChallenges/MidpointLenses.lean:44 (same declaration text).

  10. theorem OAI.SegmentLenses.SegmentFamily.norm_column_le line 69
  11. def OAI.SegmentLenses.SegmentFamily.test line 94

    Also declared: ComparatorChallenges/MidpointLenses.lean:47 (same declaration text).

  12. theorem OAI.SegmentLenses.SegmentFamily.test_apply line 97
  13. theorem OAI.SegmentLenses.SegmentFamily.norm_test_le line 115
  14. def OAI.SegmentLenses.SegmentFamily.seminorm line 129

    Also declared: ComparatorChallenges/MidpointLenses.lean:50 (same declaration text).

  15. theorem OAI.SegmentLenses.SegmentFamily.seminorm_sq line 132
  16. def OAI.SegmentLenses.SegmentFamily.singleton line 139

    Also declared: ComparatorChallenges/MidpointLenses.lean:53 (same declaration text).

  17. theorem OAI.SegmentLenses.SegmentFamily.singleton_seminorm line 151
  18. def OAI.SegmentLenses.segmentSeminorm line 165

    Also declared: ComparatorChallenges/MidpointLenses.lean:67 (same declaration text).

  19. theorem OAI.SegmentLenses.segmentTests_bdd line 168
  20. theorem OAI.SegmentLenses.segmentSeminorm_apply line 175
  21. theorem OAI.SegmentLenses.le_segmentSeminorm line 179
  22. theorem OAI.SegmentLenses.abs_coord_le line 184
  23. theorem OAI.SegmentLenses.segmentSeminorm_eq_zero line 190
  24. theorem OAI.SegmentLenses.indexed_test_bound line 203
  25. theorem OAI.SegmentLenses.refinement_test_bound line 239
  26. def OAI.SegmentLenses.Test line 275

    Also declared: ComparatorChallenges/MidpointLenses.lean:70 (same declaration text).

  27. instance OAI.SegmentLenses.Test.(instance at line 279) line 279
  28. instance OAI.SegmentLenses.Test.(instance at line 280) line 280
  29. def OAI.SegmentLenses.Test.coeff line 282

    Also declared: ComparatorChallenges/MidpointLenses.lean:78 (same declaration text).

  30. def OAI.SegmentLenses.Test.ofFinsupp line 284

    Also declared: ComparatorChallenges/MidpointLenses.lean:80 (same declaration text).

  31. instance OAI.SegmentLenses.Test.(instance at line 287) line 287
  32. theorem OAI.SegmentLenses.Test.normCore line 289
  33. instance OAI.SegmentLenses.Test.(instance at line 295) line 295
  34. instance OAI.SegmentLenses.Test.(instance at line 392) line 392
  35. def OAI.SegmentLenses.Test.evaluation line 396

    Also declared: ComparatorChallenges/MidpointLenses.lean:185 (same declaration text).

  36. abbrev OAI.SegmentLenses.Primal line 489

    Also declared: ComparatorChallenges/MidpointLenses.lean:277 (same declaration text).

  37. abbrev OAI.SegmentLenses.FullDual line 493

    Also declared: ComparatorChallenges/MidpointLenses.lean:279 (same declaration text).

  38. def OAI.SegmentLenses.unitVector line 496

    Also declared: ComparatorChallenges/MidpointLenses.lean:281 (same declaration text).

  39. def OAI.SegmentLenses.coordinate line 500

    Also declared: ComparatorChallenges/MidpointLenses.lean:284 (same declaration text).

  40. def OAI.SegmentLenses.coordinateSpan line 504

    Also declared: ComparatorChallenges/MidpointLenses.lean:287 (same declaration text).

  41. abbrev OAI.SegmentLenses.CoordinatePredual line 508

    Also declared: ComparatorChallenges/MidpointLenses.lean:290 (same declaration text).

  42. def OAI.SegmentLenses.head line 511

    Also declared: ComparatorChallenges/MidpointLenses.lean:292 (same declaration text).

  43. def OAI.SegmentLenses.tail line 516

    Also declared: ComparatorChallenges/MidpointLenses.lean:295 (same declaration text).

  44. theorem OAI.SegmentLenses.prefix_antisymm line 519
  45. instance OAI.SegmentLenses.infiniteSegments line 523

    Also declared: ComparatorChallenges/MidpointLenses.lean:298 (same declaration text).

  46. theorem OAI.SegmentLenses.forestAncestor_refl line 534
  47. theorem OAI.SegmentLenses.forestAncestor_antisymm line 537
  48. instance OAI.SegmentLenses.forestSegments line 542

    Also declared: ComparatorChallenges/MidpointLenses.lean:309 (same declaration text).

  49. abbrev OAI.SegmentLenses.J line 554

    Also declared: ComparatorChallenges/MidpointLenses.lean:320 (same declaration text).

  50. abbrev OAI.SegmentLenses.X line 556

    Also declared: ComparatorChallenges/MidpointLenses.lean:322 (same declaration text).

  51. abbrev OAI.SegmentLenses.JInfinite line 558

    Also declared: ComparatorChallenges/MidpointLenses.lean:324 (same declaration text).

  52. abbrev OAI.SegmentLenses.BInfinite line 560

    Also declared: ComparatorChallenges/MidpointLenses.lean:326 (same declaration text).