OAI/Analysis/ForestSpace/Projections.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ForestSpace.headJ line 17

   Source documentation

   Completion of restriction to an ancestral head.

   noncomputable def headJ (H : Set V) (hH : IsLowerSet H) : J V →L[ℝ] J V :=
   …

   Mentions: OAI.ForestSpace.J

2. theorem OAI.ForestSpace.headJ_coe line 21
3. def OAI.ForestSpace.tailJ line 27
4. theorem OAI.ForestSpace.tailJ_coe line 30
5. theorem OAI.ForestSpace.norm_headJ_le line 38
6. theorem OAI.ForestSpace.norm_tailJ_le line 45
7. def OAI.ForestSpace.P line 52
8. def OAI.ForestSpace.Q line 55
9. theorem OAI.ForestSpace.P_coe line 58
10. theorem OAI.ForestSpace.Q_coe line 63
11. theorem OAI.ForestSpace.Q_eq_sub line 68
12. theorem OAI.ForestSpace.norm_P_le line 73
13. theorem OAI.ForestSpace.norm_Q_le line 79
14. theorem OAI.ForestSpace.annihilates_P line 85
15. theorem OAI.ForestSpace.annihilates_Q line 91
16. theorem OAI.ForestSpace.P_finite_eq_sum line 97
17. theorem OAI.ForestSpace.P_eStar line 112
18. theorem OAI.ForestSpace.P_finite_mem_span line 121
19. def OAI.ForestSpace.PX line 128

    Source documentation

    Finite ancestral heads preserve the coordinate completion by their explicit finite-coordinate formula; tails then do so by subtraction.

    noncomputable def PX (H : Finset V) (hH : IsLowerSet (H : Set V)) : X V →L[ℝ] X V :=
    …

    Mentions: OAI.ForestSpace.X

20. def OAI.ForestSpace.QX line 132
21. theorem OAI.ForestSpace.PX_val line 135
22. theorem OAI.ForestSpace.QX_val line 138
23. theorem OAI.ForestSpace.norm_PX_le line 142
24. theorem OAI.ForestSpace.norm_QX_le line 145
25. theorem OAI.ForestSpace.finite_span_support line 151
26. theorem OAI.ForestSpace.exists_head_approx line 166

    Source documentation

    Coordinate density plus tail contractivity gives arbitrarily close finite ancestral heads in the general coordinate completion.

     theorem exists_head_approx (hAnc : ∀ v : V, (Set.Iic v).Finite)
        (x : X V) (ε : ℝ) (hε : 0 < ε) :
        ∃ H : Finset V, ∃ hH : IsLowerSet (H : Set V), ‖x - PX H hH x‖ < ε := by
    …

    Mentions: OAI.ForestSpace.X, OAI.ForestSpace.PX

27. def OAI.ForestSpace.finiteCoordinates line 184

    Source documentation

    Restriction to finitely many coordinate values. Its kernel is the particular closed finite-codimensional subspace used for the modulus.

    noncomputable def finiteCoordinates (H : Finset V) : X V →L[ℝ] (H → ℝ) :=
    …

    Mentions: OAI.ForestSpace.X

28. theorem OAI.ForestSpace.finiteCoordinates_apply line 188
29. theorem OAI.ForestSpace.finiteCoordinates_kernel_finite line 191
30. theorem OAI.ForestSpace.P_eq_zero_of_mem_ker_coordinates line 195
31. theorem OAI.ForestSpace.annihilates_of_mem_ker_coordinates line 206
32. theorem OAI.ForestSpace.paired_X line 214
33. theorem OAI.ForestSpace.paired_X_two_parameters line 227
34. def OAI.ForestSpace.eX line 246
35. theorem OAI.ForestSpace.eX_val line 249
36. theorem OAI.ForestSpace.norm_eX line 250
37. theorem OAI.ForestSpace.linearIndependent_eStar line 252
38. theorem OAI.ForestSpace.linearIndependent_eX line 260
39. theorem OAI.ForestSpace.not_finiteDimensional_X line 263
40. instance OAI.ForestSpace.(instance at line 269) line 269
41. instance OAI.ForestSpace.(instance at line 278) line 278
42. theorem OAI.ForestSpace.separable_X line 283