OAI/Combinatorics/TreewidthL1/ParticleLaws.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BoundedTreewidthL1.ParticleLaws.singleton_sum line 13
  2. lemma OAI.BoundedTreewidthL1.ParticleLaws.measure_marginal line 23
  3. lemma OAI.BoundedTreewidthL1.ParticleLaws.real_sum line 34
  4. lemma OAI.BoundedTreewidthL1.ParticleLaws.symmetrize_mass line 40
  5. lemma OAI.BoundedTreewidthL1.ParticleLaws.symmetrize_flip line 51
  6. def OAI.BoundedTreewidthL1.ParticleLaws.particleMeasure line 64
  7. instance OAI.BoundedTreewidthL1.ParticleLaws.particleMeasure_finite line 67
  8. lemma OAI.BoundedTreewidthL1.ParticleLaws.particleTrace_eq line 72
  9. instance OAI.BoundedTreewidthL1.ParticleLaws.particleTrace_finite line 79
  10. lemma OAI.BoundedTreewidthL1.ParticleLaws.particle_mass line 84
  11. lemma OAI.BoundedTreewidthL1.ParticleLaws.particle_flip line 91
  12. lemma OAI.BoundedTreewidthL1.ParticleLaws.symmetrize_separation line 104
  13. lemma OAI.BoundedTreewidthL1.ParticleLaws.particle_separation line 118
  14. lemma OAI.BoundedTreewidthL1.ParticleLaws.trace_mass line 126
  15. lemma OAI.BoundedTreewidthL1.ParticleLaws.trace_flip line 131
  16. lemma OAI.BoundedTreewidthL1.ParticleLaws.flip_point_mass line 138
  17. lemma OAI.BoundedTreewidthL1.ParticleLaws.marginal_test line 149
  18. lemma OAI.BoundedTreewidthL1.ParticleLaws.separation_of_marginal line 161
  19. lemma OAI.BoundedTreewidthL1.ParticleLaws.trace_separation line 177
  20. lemma OAI.BoundedTreewidthL1.ParticleLaws.overlapping_traces line 190
  21. lemma OAI.BoundedTreewidthL1.ParticleLaws.norm_bound_from_edges line 225
  22. lemma OAI.BoundedTreewidthL1.ParticleLaws.gluing_without_path line 258
  23. lemma OAI.BoundedTreewidthL1.ParticleLaws.glue_particle_measures line 285
  24. theorem OAI.BoundedTreewidthL1.ParticleLaws.particle_law_realization line 336
  25. def OAI.BoundedTreewidthL1.RootedTree.path line 397
  26. lemma OAI.BoundedTreewidthL1.RootedTree.path_isPath line 399
  27. lemma OAI.BoundedTreewidthL1.RootedTree.path_length line 401
  28. lemma OAI.BoundedTreewidthL1.RootedTree.snd_closer line 404
  29. def OAI.BoundedTreewidthL1.RootedTree.forest line 412
  30. lemma OAI.BoundedTreewidthL1.RootedTree.parent_adj line 425
  31. lemma OAI.BoundedTreewidthL1.RootedTree.parent_of_closer line 435
  32. theorem OAI.BoundedTreewidthL1.RootedTree.edge_orientation line 454

    Source documentation

    Every actual tree edge is a parent-child edge of the depth-certified forest.

    theorem edge_orientation {i j : I} (hij : T.Adj i j) :
    (forest T hT root).parent i = some j ∨ (forest T hT root).parent j = some i := by
…

    Mentions: OAI.BoundedTreewidthL1.RootedTree.forest

  33. def OAI.BoundedTreewidthL1.BagLabels.canonicalLaw line 472

    Source documentation

    Explicit prepared law: the pushforward of the normalized tree density, using the actual overlap couplings, with the convention 0/0 = 0.

    noncomputable def canonicalLaw (T : SimpleGraph I) (B : I → Set V)
    (hcover : ∀ v, ∃ i, v ∈ B i)
    (p : (i : I) → (B i → Bool) → ℝ)
    (hcons : ∀ i j, T.Adj i j → ∀ c,
      marginal (leftTrace B i j) (p i) c = marginal (rightTrace B i j) (p j) c) :
    (V → Bool) → ℝ :=
…

    Mentions: OAI.BoundedTreewidthL1.marginal, OAI.BoundedTreewidthL1.BagLabels.leftTrace, OAI.BoundedTreewidthL1.BagLabels.rightTrace

  34. lemma OAI.BoundedTreewidthL1.BagLabels.marginal_measurable line 483
  35. lemma OAI.BoundedTreewidthL1.BagLabels.pairMass_measurable line 494
  36. lemma OAI.BoundedTreewidthL1.BagLabels.canonicalLaw_measurable line 514
  37. lemma OAI.BoundedTreewidthL1.BagLabels.canonicalLaw_normalized line 538
  38. lemma OAI.BoundedTreewidthL1.ParticleLaws.trace_restrict line 560
  39. lemma OAI.BoundedTreewidthL1.ParticleLaws.trace_eq_of_subset line 567
  40. theorem OAI.BoundedTreewidthL1.TreeParticles.tree_particle_realization line 580

    Source documentation

    The active-key preparation produces actual compatible global cut laws, without assuming consistency of any sampled bag laws.

    theorem tree_particle_realization
    (G : SimpleGraph V) (hG : G.Connected) (ℓ : G.edgeSet → ℝ) (hℓ : ∀ e, 0 < ℓ e)
    (T : SimpleGraph I) (hT : T.IsTree) (root : I) (B : I → Finset V)
    (hcover : ∀ v, ∃ i, v ∈ B i)
    (hedge : ∀ u v, G.Adj u v → ∃ i, u ∈ B i ∧ v ∈ B i)
    (hrun : ∀ v, (T.induce {i | v ∈ B i}).Preconnected)
    (A : I → Finset J) (k q : ℕ) (hbag : ∀ i, (B i).card ≤ k)
    (hA : ∀ i, (A i).card ≤ q) (hN : Fintype.card ι = 2*q + k.factorial + 2)
    (L H Δ : ℝ) (hL : 0 < L) (hH : 0 < H) (hΔ : 0 < Δ)
    (g : I → J → V → ℝ)
    (hLip : ∀ i a, ∀ u v, |g i a u - g i a v| ≤ L*shortestPathDistance G ℓ u v)
    (hHeight : ∀ i a v, |g i a v| ≤ H)
…

    Mentions: OAI.BoundedTreewidthL1.shortestPathDistance

  41. lemma OAI.BoundedTreewidthL1.ParticleLaws.marginal_integral line 630
  42. theorem OAI.BoundedTreewidthL1.ParticleLaws.averaged_bag_realization line 644

    Source documentation

    Averaging local laws first preserves exactly the co-bag metric and produces an actual Markov-glued global law, not a measurable choice of random globals.

    theorem averaged_bag_realization (T : SimpleGraph I) (hT : T.IsTree) (B : I → Set V)
    (hcover : ∀ v, ∃ i, v ∈ B i)
    (hrun : ∀ v, (T.induce {i | v ∈ B i}).Preconnected)
    (ν : Measure Ω) [IsProbabilityMeasure ν]
    (μ : Ω → (i : I) → (B i → Bool) → ℝ) (m : ℝ) (hm : 0 < m)
    (hμ : ∀ ω i a, 0 ≤ μ ω i a) (hmass : ∀ ω i, (∑ a, μ ω i a) = m)
    (hint : ∀ i a, Integrable (fun ω => μ ω i a) ν)
    (hcons : ∀ ω i j, T.Adj i j → ∀ c,
      marginal (BagLabels.leftTrace B i j) (μ ω i) c =
        marginal (BagLabels.rightTrace B i j) (μ ω j) c)
    (hflip : ∀ ω i a, μ ω i (BagLabels.flip (B i) a) = μ ω i a) :
    ∃ ρ : (V → Bool) → ℝ,
…

    Mentions: OAI.BoundedTreewidthL1.marginal, OAI.BoundedTreewidthL1.BagLabels.leftTrace, OAI.BoundedTreewidthL1.BagLabels.rightTrace, OAI.BoundedTreewidthL1.BagLabels.flip

  43. theorem OAI.BoundedTreewidthL1.ParticleLaws.averaged_particle_realization line 715

    Source documentation

    Realization of the averaged prepared particle laws, with exact local average gaps. Neither global random-law choice nor global consistency is postulated. This interface applies to the actual measurable tree preparation.

    theorem averaged_particle_realization
    (G : SimpleGraph V) (hG : G.Connected) (ℓ : G.edgeSet → ℝ) (hℓ : ∀ e, 0 < ℓ e)
    (T : SimpleGraph I) (hT : T.IsTree) (B : I → Finset V)
    (hcover : ∀ v, ∃ i, v ∈ B i)
    (hedge : ∀ u v, G.Adj u v → ∃ i, u ∈ B i ∧ v ∈ B i)
    (hrun : ∀ v, (T.induce {i | v ∈ B i}).Preconnected)
    (ν : Measure Ω) [IsProbabilityMeasure ν]
    (L H Δ : ℝ) (hL : 0 < L) (hH : 0 < H) (hΔ : 0 < Δ)
    (hN : 1 ≤ Fintype.card J) (F : Ω → I → J → V → ℝ)
    (hmeas : ∀ i j v, Measurable (fun ω => F ω i j v))
    (hF : ∀ ω i, FunctionParticleReachable (shortestPathDistance G ℓ) L H (F ω i))
    (hcons : ∀ ω i j, T.Adj i j →
…

    Mentions: OAI.BoundedTreewidthL1.FunctionParticleReachable, OAI.BoundedTreewidthL1.shortestPathDistance