OAI/Analysis/ForestSpace/Completion.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ForestSpace.TestVector line 15

    Source documentation

    Finite coordinate vectors with the segment norm (a type synonym prevents clashes with any other norm on finitely supported functions).

    Also declared: ComparatorChallenges/ForestSpace.lean:226 (same declaration text).

    def TestVector (V : Type) := V →₀ ℝ
  2. def OAI.ForestSpace.segmentSeminorm line 17

    Also declared: ComparatorChallenges/ForestSpace.lean:109 (same declaration text).

  3. instance OAI.ForestSpace.TestVector.(instance at line 134) line 134
  4. instance OAI.ForestSpace.TestVector.(instance at line 135) line 135
  5. def OAI.ForestSpace.TestVector.toFinsupp line 136

    Also declared: ComparatorChallenges/ForestSpace.lean:236 (same declaration text).

  6. instance OAI.ForestSpace.TestVector.(instance at line 137) line 137
  7. theorem OAI.ForestSpace.TestVector.ext line 139
  8. theorem OAI.ForestSpace.TestVector.zero_apply line 140
  9. theorem OAI.ForestSpace.TestVector.add_apply line 141
  10. theorem OAI.ForestSpace.TestVector.smul_apply line 142
  11. theorem OAI.ForestSpace.TestVector.coe_add line 143
  12. theorem OAI.ForestSpace.TestVector.coe_smul line 144
  13. instance OAI.ForestSpace.TestVector.(instance at line 147) line 147
  14. theorem OAI.ForestSpace.TestVector.normCore line 149
  15. instance OAI.ForestSpace.TestVector.(instance at line 157) line 157
  16. instance OAI.ForestSpace.TestVector.(instance at line 238) line 238
  17. theorem OAI.ForestSpace.TestVector.norm_eq_rho line 241
  18. theorem OAI.ForestSpace.TestVector.norm_eq_source_sup line 244

    Source documentation

    The norm on the finite-support space is the nonempty-segment supremum.

    theorem norm_eq_source_sup [Nonempty V] (u : TestVector V) :
    ‖u‖ = sSup (sourceNormValues u) :=
…

    Mentions: OAI.ForestSpace.TestVector, OAI.ForestSpace.sourceNormValues

  19. theorem OAI.ForestSpace.TestVector.norm_le_iff_testBound line 248
  20. def OAI.ForestSpace.TestVector.single line 252
  21. theorem OAI.ForestSpace.TestVector.single_apply line 255
  22. theorem OAI.ForestSpace.TestVector.norm_single line 258
  23. def OAI.ForestSpace.TestVector.eval line 268

    Source documentation

    Coordinate evaluation is bounded by singleton segment tests.

    noncomputable def eval (v : V) : TestVector V →L[ℝ] ℝ :=
…

    Mentions: OAI.ForestSpace.TestVector

  24. theorem OAI.ForestSpace.TestVector.eval_apply line 278
  25. theorem OAI.ForestSpace.TestVector.eval_norm_le line 280
  26. def OAI.ForestSpace.TestVector.cut line 286

    Source documentation

    Coordinate restriction, before the boundedness hypothesis is imposed.

    noncomputable def cut (H : Set V) : TestVector V →ₗ[ℝ] TestVector V where
…

    Mentions: OAI.ForestSpace.TestVector

  27. theorem OAI.ForestSpace.TestVector.cut_apply line 292
  28. theorem OAI.ForestSpace.TestVector.cut_supported line 295
  29. theorem OAI.ForestSpace.TestVector.cut_add_compl line 299
  30. theorem OAI.ForestSpace.TestVector.cut_eq_self line 303
  31. theorem OAI.ForestSpace.TestVector.norm_cut_le line 309
  32. theorem OAI.ForestSpace.TestVector.norm_cut_compl_le line 319
  33. theorem OAI.ForestSpace.TestVector.sum_apply line 330
  34. theorem OAI.ForestSpace.TestVector.cut_finite_eq_sum line 336
  35. theorem OAI.ForestSpace.TestVector.cut_eq_zero_of_compl line 343
  36. def OAI.ForestSpace.TestVector.head line 350
  37. def OAI.ForestSpace.TestVector.tail line 353
  38. theorem OAI.ForestSpace.TestVector.head_apply line 356
  39. theorem OAI.ForestSpace.TestVector.tail_apply line 358
  40. theorem OAI.ForestSpace.TestVector.paired_correction line 361
  41. abbrev OAI.ForestSpace.J line 385

    Source documentation

    J(T), completion of the finite-support disjoint-segment norm.

    Also declared: ComparatorChallenges/ForestSpace.lean:332 (same declaration text).

    abbrev J (V : Type) [PartialOrder V] := UniformSpace.Completion (TestVector V)

    Mentions: OAI.ForestSpace.TestVector

  42. abbrev OAI.ForestSpace.FullDual line 388

    Source documentation

    The full continuous dual, used for the finite-height forest example.

    Also declared: ComparatorChallenges/ForestSpace.lean:335 (same declaration text).

    abbrev FullDual (V : Type) [PartialOrder V] := StrongDual ℝ (J V)
…

    Mentions: OAI.ForestSpace.J