OAI/Analysis/ProductSpaces/FiniteHeads.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.IndependentProducts.FiniteHead line 14

   Source documentation

   Finite predecessor-closed heads, including the root.

   structure FiniteHead where
   …

2. def OAI.IndependentProducts.FiniteHead.Boundary line 23

   Source documentation

   First-exit vertices.

   def Boundary := {e : Edge // e.val ∉ T.vertices ∧ e.val.dropLast ∈ T.vertices}

   Mentions: OAI.IndependentProducts.Edge

3. lemma OAI.IndependentProducts.FiniteHead.boundary_eq_of_prefix line 25
4. lemma OAI.IndependentProducts.FiniteHead.boundary_unique line 38
5. lemma OAI.IndependentProducts.FiniteHead.exists_boundary_prefix line 44
6. def OAI.IndependentProducts.FiniteHead.exit line 55
7. lemma OAI.IndependentProducts.FiniteHead.exit_prefix line 58
8. lemma OAI.IndependentProducts.FiniteHead.exit_eq line 61
9. def OAI.IndependentProducts.FiniteHead.ancestor line 65

   Source documentation

   The last head ancestor of any vertex.

   noncomputable def ancestor (v : Vertex) : Vertex :=
   …

   Mentions: OAI.IndependentProducts.Vertex

10. lemma OAI.IndependentProducts.FiniteHead.ancestor_mem line 68
11. lemma OAI.IndependentProducts.FiniteHead.ancestor_prefix line 74
12. lemma OAI.IndependentProducts.FiniteHead.ancestor_of_mem line 80
13. lemma OAI.IndependentProducts.FiniteHead.ancestor_of_not_mem line 83
14. lemma OAI.IndependentProducts.FiniteHead.no_boundary_prefix_head line 86
15. def OAI.IndependentProducts.FiniteHead.containing line 90

    Source documentation

    A head containing any given finite list of vertices.

    def containing (s : Finset Vertex) : FiniteHead where
    …

    Mentions: OAI.IndependentProducts.Vertex, OAI.IndependentProducts.FiniteHead

16. lemma OAI.IndependentProducts.FiniteHead.mem_containing line 107
17. lemma OAI.IndependentProducts.mem_pathEdges_iff line 118
18. lemma OAI.IndependentProducts.pathEdges_mono line 131
19. lemma OAI.IndependentProducts.self_mem_pathEdges line 135
20. lemma OAI.IndependentProducts.pathEdges_parent line 138
21. lemma OAI.IndependentProducts.self_not_mem_pathEdges_parent line 156
22. lemma OAI.IndependentProducts.measurePreserving_sampleSelector line 168

    Source documentation

    Any coordinatewise choice from independent whole samples is again a product sample. The second index is unchanged, so the selected scalar coordinates are all distinct.

    lemma measurePreserving_sampleSelector {κ : Type uκ} [Fintype κ] (s : Edge → κ) :
        MeasurePreserving (fun ω : κ → Sample => fun e => ω (s e) e)
          (Measure.pi (fun _ : κ => productMeasure μ)) (productMeasure μ) := by
    …

    Mentions: OAI.IndependentProducts.Edge, OAI.IndependentProducts.Sample, OAI.IndependentProducts.productMeasure