Documentation

BranchingProcess.Skeleton

The measurable space of subtrees #

source
@[implicit_reducible]
instance BranchingProcess.Subtree.instMeasurableSpace {N : β„•} :
MeasurableSpace (Subtree N)

The measurable structure on subtrees of 𝒩(N): the one generated by the vertex events {T | v ∈ T}. A subtree is determined by which words it contains, so these are the events a random tree has to answer, and the Οƒ-algebra they generate is the smallest making every such question measurable.

Equations
  • One or more equations did not get rendered due to their size.
source
theorem BranchingProcess.measurableSet_mem_subtree {N : β„•} (v : Word N) :
MeasurableSet {T : Subtree N | v ∈ T}

A vertex event is measurable.

source
theorem BranchingProcess.measurable_of_mem_subtree {N : β„•} {Ξ± : Type u_1} [MeasurableSpace Ξ±] {f : Ξ± β†’ Subtree N} (h : βˆ€ (v : Word N), MeasurableSet {x : Ξ± | v ∈ f x}) :
Measurable f

The criterion for a random tree. A map into subtrees is measurable exactly when every vertex event pulls back to a measurable event.

source
theorem BranchingProcess.measurable_sample {N : β„•} :
Measurable sample

The sample is a random tree: the tree cut out by an offspring field is a measurable function of the field, by measurableSet_mem_sample.

source
noncomputable def BranchingProcess.treeLaw {J N : β„•} (ΞΈ : Offspring J) :
MeasureTheory.Measure (Subtree N)

The law of the Galton-Watson tree of an offspring law: the pushforward of the law of the offspring field along the sample.

Equations
Instances For
    source
    instance BranchingProcess.isProbabilityMeasure_treeLaw {J N : β„•} (ΞΈ : Offspring J) :
    MeasureTheory.IsProbabilityMeasure (treeLaw ΞΈ)
    source
    theorem BranchingProcess.treeLaw_mem_apply {J N : β„•} (ΞΈ : Offspring J) (v : Word N) :
    (treeLaw ΞΈ) {T : Subtree N | v ∈ T} = (sampleMeasure ΞΈ) {c : Word N β†’ β„• | v ∈ sample c}

    The vertex events of the tree law are the vertex events of the field.

    The reduced law as an offspring law #

    source
    theorem BranchingProcess.Offspring.surviveWeight_vanishing {J : β„•} (ΞΈ : Offspring J) {k : β„•} (hk : J < k) :
    ΞΈ.surviveWeight k = 0

    The surviving-children weights vanish above the support bound: a root with at most J children cannot have more than J of them survive.

    source
    theorem BranchingProcess.Offspring.sum_surviveWeight {J : β„•} (ΞΈ : Offspring J) :
    βˆ‘ k ∈ Finset.range (J + 1), ΞΈ.surviveWeight k = 1

    The surviving-children weights are a probability distribution. Summing the binomial count over the number of survivors is the binomial theorem at (1-q) + q = 1, and what is left is the offspring law itself.

    source
    theorem BranchingProcess.Offspring.skeletonWeight_nonneg {J : β„•} (ΞΈ : Offspring J) (hq : ΞΈ.extinction < 1) (k : β„•) :
    0 ≀ ΞΈ.skeletonWeight k

    The reduced weights are nonnegative once the tree survives with positive probability.

    source
    theorem BranchingProcess.Offspring.skeletonWeight_vanishing {J : β„•} (ΞΈ : Offspring J) {k : β„•} (hk : J < k) :
    ΞΈ.skeletonWeight k = 0

    The reduced weights vanish above the support bound, which is therefore inherited.

    source
    theorem BranchingProcess.Offspring.sum_skeletonWeight {J : β„•} (ΞΈ : Offspring J) (hq : ΞΈ.extinction < 1) :
    βˆ‘ k ∈ Finset.range (J + 1), ΞΈ.skeletonWeight k = 1

    The reduced weights sum to one. The surviving-children weights sum to one, the weight at zero is the extinction probability, and the renormalisation by 1-q is exactly what removes it.

    source
    noncomputable def BranchingProcess.Offspring.reduced {J : β„•} (ΞΈ : Offspring J) (hq : ΞΈ.extinction < 1) :
    Offspring J

    The reduced law as an offspring law in its own right: the Harris-Sevastyanov transform of ΞΈ, of the same support bound J. This is the law the skeleton of a surviving sample branches with.

    Equations
    Instances For
      source
      @[simp]
      theorem BranchingProcess.Offspring.reduced_apply {J : β„•} (ΞΈ : Offspring J) (hq : ΞΈ.extinction < 1) (k : β„•) :
      (ΞΈ.reduced hq).mass k = ΞΈ.skeletonWeight k
      source
      noncomputable def BranchingProcess.Offspring.skeletonTail {J : β„•} (ΞΈ : Offspring J) (m : β„•) :
      ℝ

      The mass the reduced law puts on a skeleton arity above m: the probability that a skeleton vertex has more than m children.

      Equations
      Instances For
        source
        theorem BranchingProcess.Offspring.skeletonTail_nonneg {J : β„•} (ΞΈ : Offspring J) (hq : ΞΈ.extinction < 1) (m : β„•) :
        0 ≀ ΞΈ.skeletonTail m

        The tail weights are nonnegative.

        The surviving subtrees of the root, re-addressed #

        source
        noncomputable def BranchingProcess.bushOf {N : β„•} (S : Finset (Fin N)) (m : β„•) (c : Word N β†’ β„•) :
        Word N β†’ β„•

        The offspring field of the m-th surviving child subtree of a root whose surviving children are named by S, the children being ordered by the alphabet; the zero field when there are at most m of them. The junk value is never read: every statement below guards it by m < skeletonDegree c.

        Equations
        Instances For
          source
          noncomputable def BranchingProcess.bushAt {N : β„•} (c : Word N β†’ β„•) (m : β„•) :
          Word N β†’ β„•

          The m-th surviving subtree of the root: the offspring field of the subtree founded by the m-th child of the root that survives.

          Equations
          Instances For
            source
            theorem BranchingProcess.skeletonDegree_eq_card {N : β„•} (c : Word N β†’ β„•) :
            skeletonDegree c = (survivors c).card

            The skeleton degree is the number of surviving children, unfolded.

            source
            theorem BranchingProcess.bushAt_of_lt {N : β„•} {c : Word N β†’ β„•} {m : β„•} (h : m < (survivors c).card) :
            bushAt c m = fun (w : List (Fin N)) => c (((survivors c).orderEmbOfFin β‹―) ⟨m, h⟩ :: w)

            Below the skeleton degree the m-th surviving subtree is the shift of the field to the letter naming that child.

            source
            theorem BranchingProcess.orderEmbOfFin_mem_survivors {N : β„•} {c : Word N β†’ β„•} {m : β„•} (h : m < (survivors c).card) :
            ((survivors c).orderEmbOfFin β‹―) ⟨m, h⟩ ∈ survivors c

            The letter naming the m-th surviving child is one of the surviving children.

            source
            theorem BranchingProcess.survives_bushAt {N : β„•} {c : Word N β†’ β„•} {m : β„•} (h : m < skeletonDegree c) :
            Survives (bushAt c m)

            A surviving subtree survives.

            source
            theorem BranchingProcess.measurable_bushOf {N : β„•} (S : Finset (Fin N)) (m : β„•) :
            Measurable fun (c : Word N β†’ β„•) => bushOf S m c

            The m-th surviving subtree of a prescribed pattern of survivors is a measurable function of the field: it is a shift, or a constant.

            source
            theorem BranchingProcess.measurable_bushAt {N : β„•} (m : β„•) :
            Measurable fun (c : Word N β†’ β„•) => bushAt c m

            The surviving subtrees are measurable. The pattern of survivors takes finitely many values, and on each of the corresponding events the subtree is a shift.

            The skeleton as an offspring field #

            source
            noncomputable def BranchingProcess.skelSub {N : β„•} :
            (Word N β†’ β„•) β†’ Word N β†’ Word N β†’ β„•

            The subtree of the skeleton at an address. A word u is read as an address in the skeleton: its letters name successive surviving children, the letter m selecting the m-th of them, and skelSub c u is the offspring field of the subtree the address leads to.

            Equations
            Instances For
              source
              @[simp]
              theorem BranchingProcess.skelSub_nil {N : β„•} (c : Word N β†’ β„•) :
              skelSub c [] = c
              source
              @[simp]
              theorem BranchingProcess.skelSub_cons {N : β„•} (c : Word N β†’ β„•) (j : Fin N) (u : Word N) :
              skelSub c (j :: u) = skelSub (bushAt c ↑j) u
              source
              theorem BranchingProcess.skelSub_append {N : β„•} (c : Word N β†’ β„•) (u v : Word N) :
              skelSub c (u ++ v) = skelSub (skelSub c u) v

              The branching identity for addresses: following an address and then another is following their concatenation.

              source
              noncomputable def BranchingProcess.skelField {N : β„•} (c : Word N β†’ β„•) :
              Word N β†’ β„•

              The offspring field of the skeleton: the number of surviving children of the skeleton vertex an address leads to. The re-addressing is what makes the skeleton a sample again: the m-th surviving child is reached by the letter m.

              Equations
              Instances For
                source
                @[simp]
                theorem BranchingProcess.skelField_nil {N : β„•} (c : Word N β†’ β„•) :
                skelField c [] = skeletonDegree c
                source
                @[simp]
                theorem BranchingProcess.skelField_cons {N : β„•} (c : Word N β†’ β„•) (j : Fin N) (u : Word N) :
                skelField c (j :: u) = skelField (bushAt c ↑j) u
                source
                theorem BranchingProcess.skelField_comp_cons {N : β„•} (c : Word N β†’ β„•) (j : Fin N) :
                (fun (w : Word N) => skelField c (j :: w)) = skelField (bushAt c ↑j)

                The field shifted to a child of the root is the field of that surviving subtree.

                source
                theorem BranchingProcess.skelField_comp_append {N : β„•} (c : Word N β†’ β„•) (u : Word N) :
                (fun (w : Word N) => skelField c (u ++ w)) = skelField (skelSub c u)

                The field shifted to an address is the field of the subtree there.

                source
                noncomputable def BranchingProcess.skelTree {N : β„•} (c : Word N β†’ β„•) :
                Subtree N

                The skeleton, re-addressed: the tree cut out by the offspring field of the skeleton, an isomorphic copy of the skeleton of sample c inside 𝒩(N).

                Equations
                Instances For
                  source
                  theorem BranchingProcess.mem_skelTree_cons {N : β„•} {c : Word N β†’ β„•} {j : Fin N} {u : Word N} :
                  j :: u ∈ skelTree c ↔ ↑j < skeletonDegree c ∧ u ∈ skelTree (bushAt c ↑j)

                  The one-step criterion for the skeleton. An address j :: u names a skeleton vertex exactly when the root has more than j surviving children and u names a vertex of the skeleton of the j-th of them.

                  source
                  @[simp]
                  theorem BranchingProcess.nil_mem_skelTree {N : β„•} (c : Word N β†’ β„•) :
                  [] ∈ skelTree c

                  The root is a skeleton vertex exactly when the sample survives.

                  source
                  theorem BranchingProcess.subAt_skelTree {N : β„•} {c : Word N β†’ β„•} {u : Word N} (hu : u ∈ skelTree c) :
                  Descriptive.Tree.subAt (skelTree c) u = skelTree (skelSub c u)

                  The subtree of an address is again cut out by a field of the same kind.

                  Measurability of the skeleton #

                  source
                  theorem BranchingProcess.measurable_skelSub {N : β„•} (u : Word N) :
                  Measurable fun (c : Word N β†’ β„•) => skelSub c u

                  Following a fixed address is measurable.

                  source
                  theorem BranchingProcess.measurable_skelField {N : β„•} :
                  Measurable skelField

                  The offspring field of the skeleton is measurable.

                  source
                  theorem BranchingProcess.measurable_skelTree {N : β„•} :
                  Measurable skelTree

                  The skeleton is a random tree.

                  source
                  noncomputable def BranchingProcess.skeletonTreeLaw {J N : β„•} (ΞΈ : Offspring J) :
                  MeasureTheory.Measure (Subtree N)

                  The law of the skeleton: the law of the re-addressed skeleton of a sample conditioned to survive.

                  Equations
                  Instances For
                    source
                    theorem BranchingProcess.skeletonTreeLaw_mem_apply {J N : β„•} (ΞΈ : Offspring J) (v : Word N) :
                    (skeletonTreeLaw ΞΈ) {T : Subtree N | v ∈ T} = (survivalMeasure ΞΈ) {c : Word N β†’ β„• | v ∈ skelTree c}

                    The vertex events of the skeleton law are the address events of the field.

                    Singling out one surviving subtree #

                    source
                    theorem BranchingProcess.prod_ite_survivors_single {N j : β„•} (hj : j ≀ N) {S : Finset (Fin N)} (hS : S βŠ† childSet N j) {iβ‚€ : Fin N} (hiβ‚€ : iβ‚€ ∈ S) (X A B : ENNReal) :
                    (∏ i : Fin N, if i = iβ‚€ then X else if i ∈ S then A else if ↑i < j then B else 1) = X * A ^ (S.card - 1) * B ^ (j - S.card)

                    The product over the children of a root with j children of a factor that is X at one distinguished surviving child, A at the other surviving ones, B at a dying one and 1 at a letter naming no child.

                    source
                    def BranchingProcess.bushBox {N : β„•} (j : β„•) (S : Finset (Fin N)) (iβ‚€ : Fin N) (A : Set (Word N β†’ β„•)) (i : Option (Fin N)) :
                    Set (Branch N i β†’ β„•)

                    The product event singling out one surviving subtree: the root has j children, those named by S found infinite subtrees, the remaining children die, and the subtree under the distinguished letter iβ‚€ additionally lies in A.

                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem BranchingProcess.bushBox_none {N : β„•} (j : β„•) (S : Finset (Fin N)) (iβ‚€ : Fin N) (A : Set (Word N β†’ β„•)) :
                      bushBox j S iβ‚€ A none = {u : Branch N none β†’ β„• | u rootIdx = j}
                      source
                      @[simp]
                      theorem BranchingProcess.bushBox_some {N : β„•} (j : β„•) (S : Finset (Fin N)) (iβ‚€ i : Fin N) (A : Set (Word N β†’ β„•)) :
                      bushBox j S iβ‚€ A (some i) = if i = iβ‚€ then {c : Word N β†’ β„• | Survives c} ∩ A else if i ∈ S then {c : Word N β†’ β„• | Survives c} else if ↑i < j then {c : Word N β†’ β„• | Β¬Survives c} else Set.univ
                      source
                      theorem BranchingProcess.measurableSet_bushBox {N : β„•} (j : β„•) (S : Finset (Fin N)) (iβ‚€ : Fin N) {A : Set (Word N β†’ β„•)} (hA : MeasurableSet A) (i : Option (Fin N)) :
                      MeasurableSet (bushBox j S iβ‚€ A i)
                      source
                      def BranchingProcess.bushOnly {N : β„•} (iβ‚€ : Fin N) (A : Set (Word N β†’ β„•)) (i : Option (Fin N)) :
                      Set (Branch N i β†’ β„•)

                      The extra factor that the distinguished subtree lies in A, as a product event.

                      Equations
                      Instances For
                        source
                        theorem BranchingProcess.bushBox_eq_inter {N j : β„•} {S : Finset (Fin N)} {iβ‚€ : Fin N} (hiβ‚€ : iβ‚€ ∈ S) (A : Set (Word N β†’ β„•)) (i : Option (Fin N)) :
                        bushBox j S iβ‚€ A i = skelBox j S i ∩ bushOnly iβ‚€ A i

                        The two product events cut out the one that singles out a surviving subtree.

                        source
                        theorem BranchingProcess.split_preimage_bushOnly {N : β„•} (iβ‚€ : Fin N) (A : Set (Word N β†’ β„•)) :
                        split ⁻¹' Set.univ.pi (bushOnly iβ‚€ A) = {c : Word N β†’ β„• | (fun (w : Word N) => c (iβ‚€ :: w)) ∈ A}

                        The extra factor, read through the splitting: it constrains the subtree under the distinguished letter.

                        source
                        theorem BranchingProcess.split_preimage_bushBox {N j : β„•} {S : Finset (Fin N)} (hS : S βŠ† childSet N j) {iβ‚€ : Fin N} (hiβ‚€ : iβ‚€ ∈ S) (A : Set (Word N β†’ β„•)) :
                        split ⁻¹' Set.univ.pi (bushBox j S iβ‚€ A) = {c : Word N β†’ β„• | c [] = j} ∩ {c : Word N β†’ β„• | survivors c = S} ∩ {c : Word N β†’ β„• | (fun (w : Word N) => c (iβ‚€ :: w)) ∈ A}

                        The product event singles out a surviving subtree. The root has j children with S the set of those founding an infinite subtree, and the subtree under the distinguished letter lies in A.

                        The law of one surviving subtree #

                        source
                        theorem BranchingProcess.sampleMeasure_survives_inter {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq : ΞΈ.extinction < 1) (A : Set (Word N β†’ β„•)) :
                        (sampleMeasure ΞΈ) ({c : Word N β†’ β„• | Survives c} ∩ A) = ENNReal.ofReal (1 - ΞΈ.extinction) * (survivalMeasure ΞΈ) A

                        The mass of the survival event splits off the conditioned law.

                        source
                        theorem BranchingProcess.sampleMeasure_root_survivors_bush {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq : ΞΈ.extinction < 1) {j : β„•} (hj : j ≀ N) {S : Finset (Fin N)} (hS : S βŠ† childSet N j) {m : β„•} (hm : m < S.card) {A : Set (Word N β†’ β„•)} (hA : MeasurableSet A) :
                        (sampleMeasure ΞΈ) ({c : Word N β†’ β„• | c [] = j} ∩ {c : Word N β†’ β„• | survivors c = S} ∩ {c : Word N β†’ β„• | bushOf S m c ∈ A}) = ENNReal.ofReal (ΞΈ.mass j) * ENNReal.ofReal (1 - ΞΈ.extinction) ^ S.card * ENNReal.ofReal ΞΈ.extinction ^ (j - S.card) * (survivalMeasure ΞΈ) A

                        The mass of a survival pattern with one subtree constrained. The root has j children of which exactly those named by S survive, and the m-th of the survivors lies in A: the splitting makes the subtrees independent, so the constrained one contributes the conditioned mass of A and the pattern the mass of sampleMeasure_root_survivors.

                        source
                        theorem BranchingProcess.sampleMeasure_root_skeletonDegree_bush {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq : ΞΈ.extinction < 1) {j : β„•} (hj : j ≀ N) {m k : β„•} (hm : m < k) {A : Set (Word N β†’ β„•)} (hA : MeasurableSet A) :
                        (sampleMeasure ΞΈ) ({c : Word N β†’ β„• | c [] = j} ∩ {c : Word N β†’ β„• | skeletonDegree c = k} ∩ {c : Word N β†’ β„• | bushAt c m ∈ A}) = ENNReal.ofReal (ΞΈ.mass j * ↑(j.choose k) * (1 - ΞΈ.extinction) ^ k * ΞΈ.extinction ^ (j - k)) * (survivalMeasure ΞΈ) A

                        The one-root count with one subtree constrained. The root has j children of which k survive and the m-th survivor lies in A: the patterns with k survivors are the k-element subsets of the j letters, and each carries the mass of sampleMeasure_root_survivors_bush.

                        source
                        theorem BranchingProcess.measurableSet_root_eq {N : β„•} (j : β„•) :
                        MeasurableSet {c : Word N β†’ β„• | c [] = j}

                        The offspring count at the root is a measurable coordinate.

                        source
                        theorem BranchingProcess.sampleMeasure_skeletonDegree_bush {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq : ΞΈ.extinction < 1) {m k : β„•} (hm : m < k) {A : Set (Word N β†’ β„•)} (hA : MeasurableSet A) :
                        (sampleMeasure ΞΈ) ({c : Word N β†’ β„• | skeletonDegree c = k} ∩ {c : Word N β†’ β„• | bushAt c m ∈ A}) = ENNReal.ofReal (ΞΈ.surviveWeight k) * (survivalMeasure ΞΈ) A

                        The count with one subtree constrained. Summing the one-root count over the offspring count at the root: the root has k surviving children and the m-th of them lies in A with probability ΞΈΜ‚_k times the conditioned mass of A.

                        source
                        theorem BranchingProcess.survivalMeasure_skeletonDegree_bush {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq : ΞΈ.extinction < 1) {m k : β„•} (hm : m < k) {A : Set (Word N β†’ β„•)} (hA : MeasurableSet A) :
                        (survivalMeasure ΞΈ) ({c : Word N β†’ β„• | skeletonDegree c = k} ∩ {c : Word N β†’ β„• | bushAt c m ∈ A}) = ENNReal.ofReal (ΞΈ.skeletonWeight k) * (survivalMeasure ΞΈ) A

                        The reduced law at the root with one subtree constrained. Conditioned on survival, the root has k skeleton children and the m-th of them lies in A with probability ΞΈΜƒ_k times the conditioned mass of A: the skeleton arity has the reduced law and the subtree is an independent copy of the conditioned sample.

                        source
                        theorem BranchingProcess.survivalMeasure_bushAt {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq : ΞΈ.extinction < 1) (m : β„•) {A : Set (Word N β†’ β„•)} (hA : MeasurableSet A) :
                        (survivalMeasure ΞΈ) ({c : Word N β†’ β„• | m < skeletonDegree c} ∩ {c : Word N β†’ β„• | bushAt c m ∈ A}) = ENNReal.ofReal (ΞΈ.skeletonTail m) * (survivalMeasure ΞΈ) A

                        The branching property of the skeleton, the skeleton half of the Harris decomposition beyond the root. Conditioned on survival, the root has more than m skeleton children with probability βˆ‘_{k>m} ΞΈΜƒ_k, and on that event the m-th surviving subtree is an independent copy of the sample conditioned on survival. Iterating this is what makes the skeleton a Galton-Watson tree with the reduced law.

                        The reduced law along an address #

                        source
                        noncomputable def BranchingProcess.Offspring.skeletonPath {J N : β„•} (ΞΈ : Offspring J) (u : Word N) :
                        ℝ

                        The mass the reduced law puts on an address: the product over the letters of u of the tail weights they impose, which is the probability that u names a skeleton vertex.

                        Equations
                        Instances For
                          source
                          @[simp]
                          theorem BranchingProcess.Offspring.skeletonPath_nil {J N : β„•} (ΞΈ : Offspring J) :
                          ΞΈ.skeletonPath [] = 1
                          source
                          @[simp]
                          theorem BranchingProcess.Offspring.skeletonPath_cons {J N : β„•} (ΞΈ : Offspring J) (j : Fin N) (u : Word N) :
                          ΞΈ.skeletonPath (j :: u) = ΞΈ.skeletonTail ↑j * ΞΈ.skeletonPath u
                          source
                          theorem BranchingProcess.Offspring.skeletonPath_nonneg {J N : β„•} (ΞΈ : Offspring J) (hq : ΞΈ.extinction < 1) (u : Word N) :
                          0 ≀ ΞΈ.skeletonPath u
                          source
                          theorem BranchingProcess.measurableSet_mem_skelTree {N : β„•} (u : Word N) :
                          MeasurableSet {c : Word N β†’ β„• | u ∈ skelTree c}

                          Naming a skeleton vertex is a measurable event.

                          source
                          theorem BranchingProcess.survivalMeasure_skelSub {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq : ΞΈ.extinction < 1) (u : Word N) {A : Set (Word N β†’ β„•)} (hA : MeasurableSet A) :
                          (survivalMeasure ΞΈ) ({c : Word N β†’ β„• | u ∈ skelTree c} ∩ {c : Word N β†’ β„• | skelSub c u ∈ A}) = ENNReal.ofReal (ΞΈ.skeletonPath u) * (survivalMeasure ΞΈ) A

                          The branching property along an address. Conditioned on survival, the address u names a skeleton vertex with probability ΞΈΜƒ-weight of the path, and on that event the skeleton subtree there is an independent copy of the conditioned sample. This is survivalMeasure_bushAt iterated down the address.

                          source
                          theorem BranchingProcess.survivalMeasure_mem_skelTree {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq : ΞΈ.extinction < 1) (u : Word N) :
                          (survivalMeasure ΞΈ) {c : Word N β†’ β„• | u ∈ skelTree c} = ENNReal.ofReal (ΞΈ.skeletonPath u)

                          The probability that an address names a skeleton vertex is the product of the tail weights of its letters.

                          source
                          theorem BranchingProcess.survivalMeasure_skelField {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq : ΞΈ.extinction < 1) (u : Word N) (k : β„•) :
                          (survivalMeasure ΞΈ) ({c : Word N β†’ β„• | u ∈ skelTree c} ∩ {c : Word N β†’ β„• | skelField c u = k}) = ENNReal.ofReal (ΞΈ.skeletonPath u) * ENNReal.ofReal (ΞΈ.skeletonWeight k)

                          The reduced law at an arbitrary skeleton vertex, the skeleton half of the Harris decomposition in full: conditioned on survival, an address names a skeleton vertex and the arity there is k with probability the path weight times ΞΈΜƒ_k. The arity at a skeleton vertex is therefore reduced-law distributed, independently of the address being present.

                          The vertex events of the two laws #

                          source
                          noncomputable def BranchingProcess.Offspring.tail {J : β„•} (ΞΈ : Offspring J) (m : β„•) :
                          ℝ

                          The mass an offspring law puts above m: the probability that a vertex has more than m children.

                          Equations
                          Instances For
                            source
                            theorem BranchingProcess.Offspring.tail_nonneg {J : β„•} (ΞΈ : Offspring J) (m : β„•) :
                            0 ≀ ΞΈ.tail m
                            source
                            theorem BranchingProcess.Offspring.tail_reduced {J : β„•} (ΞΈ : Offspring J) (hq : ΞΈ.extinction < 1) (m : β„•) :
                            (ΞΈ.reduced hq).tail m = ΞΈ.skeletonTail m

                            The tail weights of the reduced law are the tail weights of the skeleton.

                            source
                            noncomputable def BranchingProcess.Offspring.path {J N : β„•} (ΞΈ : Offspring J) (u : Word N) :
                            ℝ

                            The mass an offspring law puts on a word: the product over its letters of the tail weights they impose, which is the probability that the word lies in the sample.

                            Equations
                            Instances For
                              source
                              @[simp]
                              theorem BranchingProcess.Offspring.path_nil {J N : β„•} (ΞΈ : Offspring J) :
                              ΞΈ.path [] = 1
                              source
                              @[simp]
                              theorem BranchingProcess.Offspring.path_cons {J N : β„•} (ΞΈ : Offspring J) (j : Fin N) (u : Word N) :
                              ΞΈ.path (j :: u) = ΞΈ.tail ↑j * ΞΈ.path u
                              source
                              theorem BranchingProcess.Offspring.path_nonneg {J N : β„•} (ΞΈ : Offspring J) (u : Word N) :
                              0 ≀ ΞΈ.path u
                              source
                              theorem BranchingProcess.Offspring.path_reduced {J N : β„•} (ΞΈ : Offspring J) (hq : ΞΈ.extinction < 1) (u : Word N) :
                              (ΞΈ.reduced hq).path u = ΞΈ.skeletonPath u

                              The path weights of the reduced law are the path weights of the skeleton.

                              source
                              theorem BranchingProcess.infinitePi_root_gt {J N : β„•} (ΞΈ : Offspring J) (m : β„•) :
                              (MeasureTheory.Measure.infinitePi fun (x : Branch N none) => ΞΈ.law) {u : Branch N none β†’ β„• | m < u rootIdx} = ENNReal.ofReal (ΞΈ.tail m)

                              The root factor of the splitting for a tail event: the offspring count at the root exceeds m with probability the tail weight.

                              source
                              def BranchingProcess.pathBox {N : β„•} (j : Fin N) (E : Set (Word N β†’ β„•)) (i : Option (Fin N)) :
                              Set (Branch N i β†’ β„•)

                              The product event for a word: the root has more than j children and the subtree under the letter j lies in E.

                              Equations
                              Instances For
                                source
                                theorem BranchingProcess.measurableSet_pathBox {N : β„•} (j : Fin N) {E : Set (Word N β†’ β„•)} (hE : MeasurableSet E) (i : Option (Fin N)) :
                                MeasurableSet (pathBox j E i)
                                source
                                theorem BranchingProcess.split_preimage_pathBox {N : β„•} (j : Fin N) (E : Set (Word N β†’ β„•)) :
                                split ⁻¹' Set.univ.pi (pathBox j E) = {c : Word N β†’ β„• | ↑j < c []} ∩ {c : Word N β†’ β„• | (fun (w : Word N) => c (j :: w)) ∈ E}

                                The product event is the one-letter event. The root has more than j children and the subtree under the letter j lies in E.

                                source
                                theorem BranchingProcess.sampleMeasure_mem_sample {J N : β„•} (ΞΈ : Offspring J) (u : Word N) :
                                (sampleMeasure ΞΈ) {c : Word N β†’ β„• | u ∈ sample c} = ENNReal.ofReal (ΞΈ.path u)

                                The probability that a word lies in the sample is the product of the tail weights of its letters: each letter demands that the vertex it leaves have enough children, and the splitting makes those demands independent.

                                source
                                theorem BranchingProcess.treeLaw_mem {J N : β„•} (ΞΈ : Offspring J) (u : Word N) :
                                (treeLaw θ) {T : Subtree N | u ∈ T} = ENNReal.ofReal (θ.path u)

                                The vertex events of the Galton-Watson tree law.

                                source
                                theorem BranchingProcess.skeletonTreeLaw_mem_eq_treeLaw {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq : ΞΈ.extinction < 1) (u : Word N) :
                                (skeletonTreeLaw θ) {T : Subtree N | u ∈ T} = (treeLaw (θ.reduced hq)) {T : Subtree N | u ∈ T}

                                The skeleton is a Galton-Watson tree with the reduced law, on the vertex events. Conditioned on survival, the re-addressed skeleton contains a given word with exactly the probability that the Galton-Watson tree of the reduced law does. These events generate the measurable structure on subtrees.

                                The rank of a surviving child #

                                source
                                def BranchingProcess.rankOf {N : β„•} (S : Finset (Fin N)) (i : Fin N) :
                                β„•

                                The rank of a letter among a set of letters: the number of elements of S strictly below i. Along the surviving children this is the address the child receives in the re-addressed skeleton.

                                Equations
                                Instances For
                                  source
                                  theorem BranchingProcess.rankOf_orderEmbOfFin {N : β„•} (S : Finset (Fin N)) {k : β„•} (h : S.card = k) (m : Fin k) :
                                  rankOf S ((S.orderEmbOfFin h) m) = ↑m

                                  The enumeration of S in increasing order inverts the rank.

                                  source
                                  theorem BranchingProcess.prod_rankOf {N : β„•} {M : Type u_1} [CommMonoid M] (S : Finset (Fin N)) (f : β„• β†’ M) :
                                  ∏ i ∈ S, f (rankOf S i) = ∏ m ∈ Finset.range S.card, f m

                                  Reindexing a product over a set of letters by the rank. The ranks of the elements of S run through 0,…,|S|-1.

                                  source
                                  theorem BranchingProcess.rankOf_lt_card {N : β„•} {S : Finset (Fin N)} {i : Fin N} (hi : i ∈ S) :
                                  rankOf S i < S.card

                                  An element of S has rank below the cardinality.

                                  source
                                  theorem BranchingProcess.bushOf_rankOf {N : β„•} {S : Finset (Fin N)} {i : Fin N} (hi : i ∈ S) (c : Word N β†’ β„•) :
                                  bushOf S (rankOf S i) c = fun (w : List (Fin N)) => c (i :: w)

                                  The rank enumerates the surviving children: below the skeleton degree the m-th surviving subtree is the shift to the letter of rank m.

                                  source
                                  theorem BranchingProcess.forall_bushOf_iff {N : β„•} (S : Finset (Fin N)) (A : β„• β†’ Set (Word N β†’ β„•)) (c : Word N β†’ β„•) :
                                  (βˆ€ m < S.card, bushOf S m c ∈ A m) ↔ βˆ€ i ∈ S, (fun (w : Word N) => c (i :: w)) ∈ A (rankOf S i)

                                  The rank-indexed constraints on the surviving subtrees, read letter by letter. Constraining the m-th surviving subtree for every m below the number of survivors is constraining the subtree under each surviving letter by the set of its rank.

                                  Constraining every surviving subtree #

                                  source
                                  theorem BranchingProcess.prod_ite_survivors_family {N j : β„•} (hj : j ≀ N) {S : Finset (Fin N)} (hS : S βŠ† childSet N j) (X : β„• β†’ ENNReal) (B : ENNReal) :
                                  (∏ i : Fin N, if i ∈ S then X (rankOf S i) else if ↑i < j then B else 1) = (∏ m ∈ Finset.range S.card, X m) * B ^ (j - S.card)

                                  The product over the children of a root with j children of a factor that is X of the rank at a surviving child, B at a dying one and 1 at a letter naming no child. The ranks run through 0,…,|S|-1.

                                  source
                                  def BranchingProcess.bushesBox {N : β„•} (j : β„•) (S : Finset (Fin N)) (A : β„• β†’ Set (Word N β†’ β„•)) (i : Option (Fin N)) :
                                  Set (Branch N i β†’ β„•)

                                  The product event constraining every surviving subtree: the root has j children, those named by S found infinite subtrees, the remaining children die, and the subtree under a surviving letter lies in the set indexed by its rank.

                                  Equations
                                  Instances For
                                    source
                                    @[simp]
                                    theorem BranchingProcess.bushesBox_none {N : β„•} (j : β„•) (S : Finset (Fin N)) (A : β„• β†’ Set (Word N β†’ β„•)) :
                                    bushesBox j S A none = {u : Branch N none β†’ β„• | u rootIdx = j}
                                    source
                                    @[simp]
                                    theorem BranchingProcess.bushesBox_some {N : β„•} (j : β„•) (S : Finset (Fin N)) (A : β„• β†’ Set (Word N β†’ β„•)) (i : Fin N) :
                                    bushesBox j S A (some i) = if i ∈ S then {c : Word N β†’ β„• | Survives c} ∩ A (rankOf S i) else if ↑i < j then {c : Word N β†’ β„• | Β¬Survives c} else Set.univ
                                    source
                                    theorem BranchingProcess.measurableSet_bushesBox {N : β„•} (j : β„•) (S : Finset (Fin N)) {A : β„• β†’ Set (Word N β†’ β„•)} (hA : βˆ€ (m : β„•), MeasurableSet (A m)) (i : Option (Fin N)) :
                                    MeasurableSet (bushesBox j S A i)
                                    source
                                    def BranchingProcess.bushesOnly {N : β„•} (S : Finset (Fin N)) (A : β„• β†’ Set (Word N β†’ β„•)) (i : Option (Fin N)) :
                                    Set (Branch N i β†’ β„•)

                                    The extra factors constraining the surviving subtrees, as a product event.

                                    Equations
                                    Instances For
                                      source
                                      theorem BranchingProcess.bushesBox_eq_inter {N : β„•} (j : β„•) (S : Finset (Fin N)) (A : β„• β†’ Set (Word N β†’ β„•)) (i : Option (Fin N)) :
                                      bushesBox j S A i = skelBox j S i ∩ bushesOnly S A i

                                      The two product events cut out the one constraining every surviving subtree.

                                      source
                                      theorem BranchingProcess.split_preimage_bushesOnly {N : β„•} (S : Finset (Fin N)) (A : β„• β†’ Set (Word N β†’ β„•)) :
                                      split ⁻¹' Set.univ.pi (bushesOnly S A) = {c : Word N β†’ β„• | βˆ€ i ∈ S, (fun (w : Word N) => c (i :: w)) ∈ A (rankOf S i)}

                                      The extra factors, read through the splitting.

                                      source
                                      theorem BranchingProcess.split_preimage_bushesBox {N j : β„•} {S : Finset (Fin N)} (hS : S βŠ† childSet N j) (A : β„• β†’ Set (Word N β†’ β„•)) :
                                      split ⁻¹' Set.univ.pi (bushesBox j S A) = {c : Word N β†’ β„• | c [] = j} ∩ {c : Word N β†’ β„• | survivors c = S} ∩ {c : Word N β†’ β„• | βˆ€ m < S.card, bushOf S m c ∈ A m}

                                      The product event constrains every surviving subtree.

                                      source
                                      noncomputable def BranchingProcess.Offspring.tailGe {J : β„•} (ΞΈ : Offspring J) (n : β„•) :
                                      ℝ

                                      The mass an offspring law puts on the arities at least n.

                                      Equations
                                      Instances For
                                        source
                                        theorem BranchingProcess.Offspring.tailGe_nonneg {J : β„•} (ΞΈ : Offspring J) (n : β„•) :
                                        0 ≀ ΞΈ.tailGe n
                                        source
                                        @[simp]
                                        theorem BranchingProcess.Offspring.tailGe_zero {J : β„•} (ΞΈ : Offspring J) :
                                        ΞΈ.tailGe 0 = 1

                                        No demand at all is the whole mass.

                                        source
                                        theorem BranchingProcess.Offspring.tailGe_succ {J : β„•} (ΞΈ : Offspring J) (m : β„•) :
                                        ΞΈ.tailGe (m + 1) = ΞΈ.tail m

                                        The two tails agree off zero.

                                        source
                                        theorem BranchingProcess.Offspring.tailGe_reduced_succ {J : β„•} (ΞΈ : Offspring J) (hq : ΞΈ.extinction < 1) (m : β„•) :
                                        (ΞΈ.reduced hq).tailGe (m + 1) = ΞΈ.skeletonTail m

                                        The tails of the reduced law are the skeleton tails, so the two forms of the branching property agree.

                                        The law of all the surviving subtrees #

                                        source
                                        theorem BranchingProcess.measurableSet_forall_bushOf {N : β„•} (S : Finset (Fin N)) {A : β„• β†’ Set (Word N β†’ β„•)} (hA : βˆ€ (m : β„•), MeasurableSet (A m)) :
                                        MeasurableSet {c : Word N β†’ β„• | βˆ€ m < S.card, bushOf S m c ∈ A m}

                                        Constraining every surviving subtree of a prescribed pattern is a measurable event.

                                        source
                                        theorem BranchingProcess.measurableSet_forall_bushAt {N : β„•} (k : β„•) {A : β„• β†’ Set (Word N β†’ β„•)} (hA : βˆ€ (m : β„•), MeasurableSet (A m)) :
                                        MeasurableSet {c : Word N β†’ β„• | βˆ€ m < k, bushAt c m ∈ A m}

                                        Constraining the first k surviving subtrees is a measurable event.

                                        source
                                        theorem BranchingProcess.sampleMeasure_root_survivors_bushes {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq : ΞΈ.extinction < 1) {j : β„•} (hj : j ≀ N) {S : Finset (Fin N)} (hS : S βŠ† childSet N j) {A : β„• β†’ Set (Word N β†’ β„•)} (hA : βˆ€ (m : β„•), MeasurableSet (A m)) :
                                        (sampleMeasure ΞΈ) ({c : Word N β†’ β„• | c [] = j} ∩ {c : Word N β†’ β„• | survivors c = S} ∩ {c : Word N β†’ β„• | βˆ€ m < S.card, bushOf S m c ∈ A m}) = ENNReal.ofReal (ΞΈ.mass j) * ENNReal.ofReal (1 - ΞΈ.extinction) ^ S.card * ENNReal.ofReal ΞΈ.extinction ^ (j - S.card) * ∏ m ∈ Finset.range S.card, (survivalMeasure ΞΈ) (A m)

                                        The mass of a survival pattern with every surviving subtree constrained. The splitting makes the subtrees independent, so each contributes the conditioned mass of the set of its rank and the pattern contributes the mass of sampleMeasure_root_survivors.

                                        source
                                        theorem BranchingProcess.sampleMeasure_root_skeletonDegree_bushes {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq : ΞΈ.extinction < 1) {j : β„•} (hj : j ≀ N) (k : β„•) {A : β„• β†’ Set (Word N β†’ β„•)} (hA : βˆ€ (m : β„•), MeasurableSet (A m)) :
                                        (sampleMeasure ΞΈ) ({c : Word N β†’ β„• | c [] = j} ∩ {c : Word N β†’ β„• | skeletonDegree c = k} ∩ {c : Word N β†’ β„• | βˆ€ m < k, bushAt c m ∈ A m}) = ENNReal.ofReal (ΞΈ.mass j * ↑(j.choose k) * (1 - ΞΈ.extinction) ^ k * ΞΈ.extinction ^ (j - k)) * ∏ m ∈ Finset.range k, (survivalMeasure ΞΈ) (A m)

                                        The one-root count with every surviving subtree constrained.

                                        source
                                        theorem BranchingProcess.sampleMeasure_skeletonDegree_bushes {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq : ΞΈ.extinction < 1) (k : β„•) {A : β„• β†’ Set (Word N β†’ β„•)} (hA : βˆ€ (m : β„•), MeasurableSet (A m)) :
                                        (sampleMeasure ΞΈ) ({c : Word N β†’ β„• | skeletonDegree c = k} ∩ {c : Word N β†’ β„• | βˆ€ m < k, bushAt c m ∈ A m}) = ENNReal.ofReal (ΞΈ.surviveWeight k) * ∏ m ∈ Finset.range k, (survivalMeasure ΞΈ) (A m)

                                        The count with every surviving subtree constrained, summed over the offspring count at the root.

                                        source
                                        theorem BranchingProcess.survivalMeasure_skeletonDegree_bushes {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq : ΞΈ.extinction < 1) (k : β„•) {A : β„• β†’ Set (Word N β†’ β„•)} (hA : βˆ€ (m : β„•), MeasurableSet (A m)) :
                                        (survivalMeasure ΞΈ) ({c : Word N β†’ β„• | skeletonDegree c = k} ∩ {c : Word N β†’ β„• | βˆ€ m < k, bushAt c m ∈ A m}) = ENNReal.ofReal (ΞΈ.skeletonWeight k) * ∏ m ∈ Finset.range k, (survivalMeasure ΞΈ) (A m)

                                        The reduced law at the root with every surviving subtree constrained. Conditioned on survival, the root has k skeleton children with probability ΞΈΜƒ_k, and the k subtrees are independent copies of the conditioned sample.

                                        source
                                        theorem BranchingProcess.survivalMeasure_bushes {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq : ΞΈ.extinction < 1) (n : β„•) {A : β„• β†’ Set (Word N β†’ β„•)} (hA : βˆ€ (m : β„•), MeasurableSet (A m)) (hAtop : βˆ€ (m : β„•), n ≀ m β†’ A m = Set.univ) :
                                        (survivalMeasure ΞΈ) ({c : Word N β†’ β„• | n ≀ skeletonDegree c} ∩ {c : Word N β†’ β„• | βˆ€ m < skeletonDegree c, bushAt c m ∈ A m}) = ENNReal.ofReal ((ΞΈ.reduced hq).tailGe n) * ∏ m ∈ Finset.range n, (survivalMeasure ΞΈ) (A m)

                                        The branching property of the skeleton with every subtree constrained. Conditioned on survival, the root has at least n skeleton children with probability βˆ‘_{kβ‰₯n} ΞΈΜƒ_k, and the subtrees are independent copies of the conditioned sample: the sets above n impose nothing, so only the first n factors survive.

                                        Finite prefix-closed sets of words #

                                        source
                                        def BranchingProcess.PrefixClosed {N : β„•} (F : Set (Word N)) :
                                        Prop

                                        A set of words is prefix-closed when it contains every prefix of each of its elements. These are the sets a subtree can contain, and the events {T | F βŠ† T} they name are the Ο€-system the two laws are compared on.

                                        Equations
                                        Instances For
                                          source
                                          def BranchingProcess.wordSub {N : β„•} (F : Set (Word N)) (m : β„•) :
                                          Set (Word N)

                                          The residual set at the letter of index m: the words u with the m-th letter prepended lying in F. Empty once m names no letter.

                                          Equations
                                          Instances For
                                            source
                                            theorem BranchingProcess.mem_wordSub {N : β„•} {F : Set (Word N)} {i : Fin N} {u : Word N} :
                                            u ∈ wordSub F ↑i ↔ i :: u ∈ F

                                            The residual set at an actual letter.

                                            source
                                            theorem BranchingProcess.PrefixClosed.wordSub {N : β„•} {F : Set (Word N)} (hF : PrefixClosed F) (m : β„•) :
                                            PrefixClosed (BranchingProcess.wordSub F m)

                                            Residual sets inherit prefix closure.

                                            source
                                            theorem BranchingProcess.length_le_of_mem_wordSub {N : β„•} {F : Set (Word N)} {n m : β„•} (hn : βˆ€ v ∈ F, List.length v ≀ n + 1) {u : Word N} (hu : u ∈ wordSub F m) :
                                            List.length u ≀ n

                                            Residual sets are one generation shorter.

                                            source
                                            noncomputable def BranchingProcess.rootDeg {N : β„•} (F : Set (Word N)) :
                                            β„•

                                            The offspring count a prefix-closed set demands at the root: one more than the largest letter it uses there.

                                            Equations
                                            Instances For
                                              source
                                              theorem BranchingProcess.lt_rootDeg {N : β„•} {F : Set (Word N)} {i : Fin N} (hi : [i] ∈ F) :
                                              ↑i < rootDeg F

                                              A letter used at the root lies below the demanded count.

                                              source
                                              theorem BranchingProcess.rootDeg_le_iff {N : β„•} {F : Set (Word N)} {k : β„•} :
                                              rootDeg F ≀ k ↔ βˆ€ (i : Fin N), [i] ∈ F β†’ ↑i < k

                                              The demanded count is what makes every letter used at the root available.

                                              source
                                              theorem BranchingProcess.rootDeg_le_card {N : β„•} (F : Set (Word N)) :
                                              rootDeg F ≀ N

                                              The alphabet carries the demand at the root.

                                              source
                                              theorem BranchingProcess.wordSub_eq_empty {N : β„•} {F : Set (Word N)} (hF : PrefixClosed F) {m : β„•} (hm : rootDeg F ≀ m) :
                                              wordSub F m = βˆ…

                                              Above the demanded count the residual sets are empty.

                                              source
                                              theorem BranchingProcess.subset_skelTree_iff {N : β„•} {F : Set (Word N)} (hF : PrefixClosed F) (c : Word N β†’ β„•) :
                                              F βŠ† ↑(skelTree c) ↔ rootDeg F ≀ skeletonDegree c ∧ βˆ€ m < skeletonDegree c, wordSub F m βŠ† ↑(skelTree (bushAt c m))

                                              The one-step criterion for containment in the skeleton.

                                              source
                                              theorem BranchingProcess.subset_sample_iff {N : β„•} {F : Set (Word N)} (hF : PrefixClosed F) (c : Word N β†’ β„•) :
                                              F βŠ† ↑(sample c) ↔ rootDeg F ≀ c [] ∧ βˆ€ (i : Fin N), wordSub F ↑i βŠ† ↑(sample fun (w : Word N) => c (i :: w))

                                              The one-step criterion for containment in a sample.

                                              source
                                              theorem BranchingProcess.measurableSet_subset_skelTree {N : β„•} (G : Set (Word N)) :
                                              MeasurableSet {c : Word N β†’ β„• | G βŠ† ↑(skelTree c)}

                                              Containment in the skeleton is a measurable event: a countable intersection of the address events, Word N being countable.

                                              source
                                              theorem BranchingProcess.measurableSet_subset_sample {N : β„•} (G : Set (Word N)) :
                                              MeasurableSet {c : Word N β†’ β„• | G βŠ† ↑(sample c)}

                                              Containment in the sample is a measurable event.

                                              source
                                              theorem BranchingProcess.measurableSet_subset_subtree {N : β„•} (G : Set (Word N)) :
                                              MeasurableSet {T : Subtree N | G βŠ† ↑T}

                                              Containment is a measurable event on subtrees.

                                              The two recursions #

                                              source
                                              theorem BranchingProcess.infinitePi_root_ge {J N : β„•} (ΞΈ : Offspring J) (n : β„•) :
                                              (MeasureTheory.Measure.infinitePi fun (x : Branch N none) => ΞΈ.law) {u : Branch N none β†’ β„• | n ≀ u rootIdx} = ENNReal.ofReal (ΞΈ.tailGe n)

                                              The root factor of the splitting for a demand at the root.

                                              source
                                              def BranchingProcess.subsetBox {N : β„•} (F : Set (Word N)) (i : Option (Fin N)) :
                                              Set (Branch N i β†’ β„•)

                                              The product event for containment: the root has enough children and each subtree contains the corresponding residual set.

                                              Equations
                                              Instances For
                                                source
                                                theorem BranchingProcess.measurableSet_subsetBox {N : β„•} (F : Set (Word N)) (i : Option (Fin N)) :
                                                MeasurableSet (subsetBox F i)
                                                source
                                                theorem BranchingProcess.split_preimage_subsetBox {N : β„•} {F : Set (Word N)} (hF : PrefixClosed F) :
                                                split ⁻¹' Set.univ.pi (subsetBox F) = {c : Word N β†’ β„• | F βŠ† ↑(sample c)}

                                                The product event is containment.

                                                source
                                                theorem BranchingProcess.sampleMeasure_subset_sample_step {J N : β„•} (ΞΈ : Offspring J) {F : Set (Word N)} (hF : PrefixClosed F) :
                                                (sampleMeasure ΞΈ) {c : Word N β†’ β„• | F βŠ† ↑(sample c)} = ENNReal.ofReal (ΞΈ.tailGe (rootDeg F)) * ∏ i : Fin N, (sampleMeasure ΞΈ) {d : Word N β†’ β„• | wordSub F ↑i βŠ† ↑(sample d)}

                                                The recursion for a sample. The root must carry the demand of F, and the subtrees must carry the residual sets, independently.

                                                source
                                                theorem BranchingProcess.survivalMeasure_subset_skelTree_step {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq : ΞΈ.extinction < 1) {F : Set (Word N)} (hF : PrefixClosed F) :
                                                (survivalMeasure ΞΈ) {c : Word N β†’ β„• | F βŠ† ↑(skelTree c)} = ENNReal.ofReal ((ΞΈ.reduced hq).tailGe (rootDeg F)) * ∏ m ∈ Finset.range (rootDeg F), (survivalMeasure ΞΈ) {d : Word N β†’ β„• | wordSub F m βŠ† ↑(skelTree d)}

                                                The recursion for the skeleton. Conditioned on survival, the root must have enough skeleton children to carry the demand of F, and the surviving subtrees must carry the residual sets, independently.

                                                The pushforward #

                                                source
                                                theorem BranchingProcess.survivalMeasure_subset_skelTree {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq : ΞΈ.extinction < 1) (n : β„•) (F : Set (Word N)) :
                                                PrefixClosed F β†’ (βˆ€ v ∈ F, List.length v ≀ n) β†’ (survivalMeasure ΞΈ) {c : Word N β†’ β„• | F βŠ† ↑(skelTree c)} = (sampleMeasure (ΞΈ.reduced hq)) {c : Word N β†’ β„• | F βŠ† ↑(sample c)}

                                                The skeleton is a Galton-Watson tree with the reduced law, on every finite prefix-closed set of words. Both sides satisfy the same recursion, the skeleton one by survivalMeasure_subset_skelTree_step and the sample one by sampleMeasure_subset_sample_step, so the induction on the height of F closes.

                                                source
                                                theorem BranchingProcess.finite_prefixes {N : β„•} (v : Word N) :
                                                {u : Word N | u <+: v}.Finite

                                                The set of prefixes of a word is finite.

                                                source
                                                theorem BranchingProcess.prefixClosed_prefixes {N : β„•} (v : Word N) :
                                                PrefixClosed {u : Word N | u <+: v}

                                                The set of prefixes of a word is prefix-closed.

                                                source
                                                theorem BranchingProcess.mem_subtree_eq_subset {N : β„•} (v : Word N) :
                                                {T : Subtree N | v ∈ T} = {T : Subtree N | {u : Word N | u <+: v} βŠ† ↑T}

                                                A vertex event is a containment event, subtrees being prefix-closed.

                                                source
                                                def BranchingProcess.containmentSets (N : β„•) :
                                                Set (Set (Subtree N))

                                                The containment events of the finite prefix-closed sets of words.

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  source
                                                  theorem BranchingProcess.isPiSystem_containmentSets {N : β„•} :
                                                  IsPiSystem (containmentSets N)

                                                  The containment events form a Ο€-system: the union of two finite prefix-closed sets of words is finite and prefix-closed.

                                                  source
                                                  theorem BranchingProcess.generateFrom_containmentSets {N : β„•} :
                                                  Subtree.instMeasurableSpace = MeasurableSpace.generateFrom (containmentSets N)

                                                  The containment events generate the measurable structure on subtrees.

                                                  source
                                                  theorem BranchingProcess.skeletonTreeLaw_eq_treeLaw {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq : ΞΈ.extinction < 1) :
                                                  skeletonTreeLaw ΞΈ = treeLaw (ΞΈ.reduced hq)

                                                  The Harris recursion, the skeleton half of the decomposition in full. Conditioned on survival, the re-addressed skeleton of the sample is a Galton-Watson tree with the reduced law of the Harris-Sevastyanov transform. The containment events of the finite prefix-closed sets of words form a Ο€-system generating the measurable structure on subtrees, and the two laws agree on it.

                                                  The conjugate law of the bushes #

                                                  source
                                                  noncomputable def BranchingProcess.Offspring.conjugateWeight {J : β„•} (ΞΈ : Offspring J) (j : β„•) :
                                                  ℝ

                                                  The conjugate law of the bush half of the Harris decomposition: the offspring law tilted by the extinction probability, ΞΈ_j q^j / q. This is the law a subtree conditioned to die branches with.

                                                  Equations
                                                  Instances For
                                                    source
                                                    theorem BranchingProcess.Offspring.conjugateWeight_nonneg {J : β„•} (ΞΈ : Offspring J) (j : β„•) :
                                                    0 ≀ ΞΈ.conjugateWeight j
                                                    source
                                                    theorem BranchingProcess.Offspring.conjugateWeight_vanishing {J : β„•} (ΞΈ : Offspring J) {j : β„•} (hj : J < j) :
                                                    ΞΈ.conjugateWeight j = 0
                                                    source
                                                    theorem BranchingProcess.Offspring.sum_conjugateWeight {J : β„•} (ΞΈ : Offspring J) (hq0 : 0 < ΞΈ.extinction) :
                                                    βˆ‘ j ∈ Finset.range (J + 1), ΞΈ.conjugateWeight j = 1

                                                    The conjugate weights sum to one: the generating function is at its fixed point, so the tilt is exactly normalised.

                                                    source
                                                    noncomputable def BranchingProcess.Offspring.conjugate {J : β„•} (ΞΈ : Offspring J) (hq0 : 0 < ΞΈ.extinction) :
                                                    Offspring J

                                                    The conjugate law as an offspring law in its own right, of the same support bound J. This is the law a bush branches with.

                                                    Equations
                                                    Instances For
                                                      source
                                                      @[simp]
                                                      theorem BranchingProcess.Offspring.conjugate_apply {J : β„•} (ΞΈ : Offspring J) (hq0 : 0 < ΞΈ.extinction) (j : β„•) :
                                                      (ΞΈ.conjugate hq0).mass j = ΞΈ.conjugateWeight j

                                                      The law of a bush #

                                                      source
                                                      theorem BranchingProcess.sampleMeasure_notSurvives_ne_zero {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq0 : 0 < ΞΈ.extinction) :
                                                      (sampleMeasure ΞΈ) {c : Word N β†’ β„• | Β¬Survives c} β‰  0

                                                      The conditioning event has positive mass exactly for q > 0.

                                                      source
                                                      theorem BranchingProcess.isProbabilityMeasure_bushMeasure {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq0 : 0 < ΞΈ.extinction) :
                                                      MeasureTheory.IsProbabilityMeasure (bushMeasure ΞΈ)

                                                      The bush law is a probability measure once the tree dies with positive probability.

                                                      source
                                                      theorem BranchingProcess.bushMeasure_apply {J N : β„•} (ΞΈ : Offspring J) (t : Set (Word N β†’ β„•)) :
                                                      (bushMeasure ΞΈ) t = ((sampleMeasure ΞΈ) {c : Word N β†’ β„• | Β¬Survives c})⁻¹ * (sampleMeasure ΞΈ) ({c : Word N β†’ β„• | Β¬Survives c} ∩ t)

                                                      The bush law, unfolded.

                                                      source
                                                      theorem BranchingProcess.sampleMeasure_notSurvives_inter {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq0 : 0 < ΞΈ.extinction) (A : Set (Word N β†’ β„•)) :
                                                      (sampleMeasure ΞΈ) ({c : Word N β†’ β„• | Β¬Survives c} ∩ A) = ENNReal.ofReal ΞΈ.extinction * (bushMeasure ΞΈ) A

                                                      The mass of the extinction event splits off the bush law.

                                                      source
                                                      noncomputable def BranchingProcess.bushTreeLaw {J N : β„•} (ΞΈ : Offspring J) :
                                                      MeasureTheory.Measure (Subtree N)

                                                      The law of the bush of a sample conditioned to die.

                                                      Equations
                                                      Instances For

                                                        Constraining every dying subtree #

                                                        source
                                                        theorem BranchingProcess.rankOf_univ {N : β„•} (i : Fin N) :
                                                        rankOf Finset.univ i = ↑i

                                                        The rank of a letter among all letters is the letter itself.

                                                        source
                                                        theorem BranchingProcess.prod_ite_childSet {N : β„•} {M : Type u_1} [CommMonoid M] {j : β„•} (X Y : Fin N β†’ M) (hY : βˆ€ (i : Fin N), ¬↑i < j β†’ Y i = 1) :
                                                        (∏ i : Fin N, if ↑i < j then X i else Y i) = ∏ i ∈ childSet N j, X i

                                                        The product over the children of a root with j children when the letters naming no child contribute nothing.

                                                        source
                                                        theorem BranchingProcess.prod_childSet {N : β„•} {M : Type u_1} [CommMonoid M] {j : β„•} (hj : j ≀ N) (f : β„• β†’ M) :
                                                        ∏ i ∈ childSet N j, f ↑i = ∏ m ∈ Finset.range j, f m

                                                        Reindexing a product over the letters naming a child by the number they name.

                                                        source
                                                        def BranchingProcess.dyingBox {N : β„•} (j : β„•) (A : β„• β†’ Set (Word N β†’ β„•)) (i : Option (Fin N)) :
                                                        Set (Branch N i β†’ β„•)

                                                        The product event constraining every dying subtree: the root has j children, all of them die, and the subtree under a letter lies in the set indexed by that letter.

                                                        Equations
                                                        Instances For
                                                          source
                                                          @[simp]
                                                          theorem BranchingProcess.dyingBox_none {N : β„•} (j : β„•) (A : β„• β†’ Set (Word N β†’ β„•)) :
                                                          dyingBox j A none = {u : Branch N none β†’ β„• | u rootIdx = j}
                                                          source
                                                          @[simp]
                                                          theorem BranchingProcess.dyingBox_some {N : β„•} (j : β„•) (A : β„• β†’ Set (Word N β†’ β„•)) (i : Fin N) :
                                                          dyingBox j A (some i) = (if ↑i < j then {c : Word N β†’ β„• | Β¬Survives c} else Set.univ) ∩ A ↑i
                                                          source
                                                          theorem BranchingProcess.measurableSet_dyingBox {N : β„•} (j : β„•) {A : β„• β†’ Set (Word N β†’ β„•)} (hA : βˆ€ (m : β„•), MeasurableSet (A m)) (i : Option (Fin N)) :
                                                          MeasurableSet (dyingBox j A i)
                                                          source
                                                          theorem BranchingProcess.dyingBox_eq_inter {N : β„•} (j : β„•) (A : β„• β†’ Set (Word N β†’ β„•)) (i : Option (Fin N)) :
                                                          dyingBox j A i = skelBox j βˆ… i ∩ bushesOnly Finset.univ A i

                                                          The dying box splits into the empty survival pattern and the constraints.

                                                          source
                                                          theorem BranchingProcess.split_preimage_dyingBox {N : β„•} (j : β„•) (A : β„• β†’ Set (Word N β†’ β„•)) :
                                                          split ⁻¹' Set.univ.pi (dyingBox j A) = {c : Word N β†’ β„• | c [] = j} ∩ {c : Word N β†’ β„• | survivors c = βˆ…} ∩ {c : Word N β†’ β„• | βˆ€ (i : Fin N), (fun (w : Word N) => c (i :: w)) ∈ A ↑i}

                                                          The product event constrains every dying subtree.

                                                          source
                                                          theorem BranchingProcess.sampleMeasure_root_dying {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq0 : 0 < ΞΈ.extinction) {n j : β„•} (hj : j ≀ N) (hnj : n ≀ j) {A : β„• β†’ Set (Word N β†’ β„•)} (hA : βˆ€ (m : β„•), MeasurableSet (A m)) (hAtop : βˆ€ (m : β„•), n ≀ m β†’ A m = Set.univ) :
                                                          (sampleMeasure ΞΈ) ({c : Word N β†’ β„• | c [] = j} ∩ {c : Word N β†’ β„• | survivors c = βˆ…} ∩ {c : Word N β†’ β„• | βˆ€ (i : Fin N), (fun (w : Word N) => c (i :: w)) ∈ A ↑i}) = ENNReal.ofReal (ΞΈ.mass j) * ENNReal.ofReal ΞΈ.extinction ^ j * ∏ m ∈ Finset.range n, (bushMeasure ΞΈ) (A m)

                                                          The mass of a dying root with every subtree constrained. The root has j children, all of the subtrees die, and each lies in the set indexed by its letter: the splitting makes them independent bushes.

                                                          source
                                                          theorem BranchingProcess.bushMeasure_dying {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq0 : 0 < ΞΈ.extinction) (n : β„•) {A : β„• β†’ Set (Word N β†’ β„•)} (hA : βˆ€ (m : β„•), MeasurableSet (A m)) (hAtop : βˆ€ (m : β„•), n ≀ m β†’ A m = Set.univ) :
                                                          (bushMeasure ΞΈ) ({c : Word N β†’ β„• | n ≀ c []} ∩ {c : Word N β†’ β„• | βˆ€ (i : Fin N), (fun (w : Word N) => c (i :: w)) ∈ A ↑i}) = ENNReal.ofReal ((ΞΈ.conjugate hq0).tailGe n) * ∏ m ∈ Finset.range n, (bushMeasure ΞΈ) (A m)

                                                          The branching property of the bushes, the bush half of the Harris decomposition. Conditioned on extinction, the root has at least n children with probability βˆ‘_{jβ‰₯n} ΞΈΜ‚_j, and the subtrees are independent bushes: the sets above n impose nothing, so only the first n factors survive.

                                                          source
                                                          theorem BranchingProcess.bushMeasure_subset_sample_step {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq0 : 0 < ΞΈ.extinction) {F : Set (Word N)} (hF : PrefixClosed F) :
                                                          (bushMeasure ΞΈ) {c : Word N β†’ β„• | F βŠ† ↑(sample c)} = ENNReal.ofReal ((ΞΈ.conjugate hq0).tailGe (rootDeg F)) * ∏ m ∈ Finset.range (rootDeg F), (bushMeasure ΞΈ) {d : Word N β†’ β„• | wordSub F m βŠ† ↑(sample d)}

                                                          The recursion for a bush. Conditioned on extinction, the root must carry the demand of F, and the dying subtrees must carry the residual sets, independently.

                                                          source
                                                          theorem BranchingProcess.bushMeasure_subset_sample {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq0 : 0 < ΞΈ.extinction) (n : β„•) (F : Set (Word N)) :
                                                          PrefixClosed F β†’ (βˆ€ v ∈ F, List.length v ≀ n) β†’ (bushMeasure ΞΈ) {c : Word N β†’ β„• | F βŠ† ↑(sample c)} = (sampleMeasure (ΞΈ.conjugate hq0)) {c : Word N β†’ β„• | F βŠ† ↑(sample c)}

                                                          The bushes are Galton-Watson trees with the conjugate law, on every finite prefix-closed set of words.

                                                          source
                                                          theorem BranchingProcess.bushTreeLaw_eq_treeLaw {J N : β„•} (ΞΈ : Offspring J) (hJN : J ≀ N) (hq0 : 0 < ΞΈ.extinction) :
                                                          bushTreeLaw ΞΈ = treeLaw (ΞΈ.conjugate hq0)

                                                          The bushes are Galton-Watson trees with the conjugate law, the bush half of the decomposition in full: conditioned on extinction, the sample is a Galton-Watson tree with the conjugate law ΞΈ_j q^j / q. Together with skeletonTreeLaw_eq_treeLaw this is the Harris decomposition: the skeleton branches with the reduced law, and what hangs off it branches with the conjugate law.