OAI/Probability/CriticalZ3/HyperedgeComparison.lean

GitHub source file

146 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperedgeComparison.Hypergraph line 16

   Source documentation

   Full labelled hyperedges; allowing empty hyperedges causes no change to clusters.

   abbrev Hypergraph (V : Type uV) (E : Type uE) := E → Set V

2. def OAI.HyperedgeComparison.Adj line 18
3. def OAI.HyperedgeComparison.Connected line 21
4. def OAI.HyperedgeComparison.cluster line 24
5. def OAI.HyperedgeComparison.clusters line 27
6. def OAI.HyperedgeComparison.Meets line 30
7. theorem OAI.HyperedgeComparison.adj_symm line 33
8. theorem OAI.HyperedgeComparison.connected_symm line 38
9. theorem OAI.HyperedgeComparison.connected_refl line 44
10. theorem OAI.HyperedgeComparison.connected_trans line 47
11. theorem OAI.HyperedgeComparison.mem_cluster_self line 51
12. theorem OAI.HyperedgeComparison.adj_mono_delete line 54
13. theorem OAI.HyperedgeComparison.cluster_mono_delete line 59
14. theorem OAI.HyperedgeComparison.clusters_mono_delete line 63
15. theorem OAI.HyperedgeComparison.clusters_contains line 68
16. theorem OAI.HyperedgeComparison.cluster_closed line 71
17. theorem OAI.HyperedgeComparison.clusters_closed line 75
18. theorem OAI.HyperedgeComparison.cluster_avoids_deleted line 80
19. theorem OAI.HyperedgeComparison.clusters_avoids_deleted line 90
20. theorem OAI.HyperedgeComparison.cluster_disjoint_clusters_iff line 99

    Source documentation

    Disjointness of a full cluster from a tested set is also disjointness from its entire union of clusters, the fact used in the first-listed-node partition.

    theorem cluster_disjoint_clusters_iff {H : Hypergraph V E} {ω : E → Bool}
        {D S : Set V} {x : V} :
        Disjoint (cluster H ω D x) (clusters H ω D S) ↔
          Disjoint (cluster H ω D x) S := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.cluster, OAI.HyperedgeComparison.clusters

21. theorem OAI.HyperedgeComparison.cluster_delete_clusters line 112

    Source documentation

    Deleting a union of clusters does not change any of the other clusters. This is deterministic, before any product-law conditioning.

    theorem cluster_delete_clusters {H : Hypergraph V E} {ω : E → Bool}
        {D S : Set V} {x : V} (hx : x ∉ clusters H ω D S) :
        cluster H ω (D ∪ clusters H ω D S) x = cluster H ω D x := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.clusters, OAI.HyperedgeComparison.cluster

22. theorem OAI.HyperedgeComparison.clusters_eq_of_agree_incident line 132

    Source documentation

    Changing bits on hyperedges disjoint from C(S) cannot change C(S). This is the key measurability assertion required for exact-cluster conditioning.

    theorem clusters_eq_of_agree_incident {H : Hypergraph V E} {ω ω' : E → Bool}
        {D S : Set V}
        (hagree : ∀ e, ¬ Disjoint (H e) (clusters H ω D S) → ω' e = ω e) :
        clusters H ω' D S = clusters H ω D S := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.clusters

23. def OAI.HyperedgeComparison.ClusterDomain line 163
24. def OAI.HyperedgeComparison.residualSample line 166
25. theorem OAI.HyperedgeComparison.residual_cluster_mem_domain line 173
26. theorem OAI.HyperedgeComparison.residual_cluster_union_mem_domain line 179
27. theorem OAI.HyperedgeComparison.residualSample_nonneg line 185
28. theorem OAI.HyperedgeComparison.residualSample_mono line 196
29. theorem OAI.HyperedgeComparison.cluster_eq_of_agree_disjoint line 227

    Source documentation

    Bits on deleted hyperedges are irrelevant to the surviving clusters.

    theorem cluster_eq_of_agree_disjoint {H : Hypergraph V E} {ω ω' : E → Bool}
        {D : Set V} (hagree : ∀ e, Disjoint (H e) D → ω' e = ω e) (s : V) :
        cluster H ω' D s = cluster H ω D s := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.cluster

30. theorem OAI.HyperedgeComparison.clusters_eq_of_agree_disjoint line 239
31. theorem OAI.HyperedgeComparison.clusters_singleton line 245
32. theorem OAI.HyperedgeComparison.clusters_delete_cluster line 251

    Source documentation

    Deleting a cluster does not change the union of any disjoint clusters.

    theorem clusters_delete_cluster {H : Hypergraph V E} {ω : E → Bool}
        {D S : Set V} {s : V} (h : Disjoint (cluster H ω D s) S) :
        clusters H ω (D ∪ cluster H ω D s) S = clusters H ω D S := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.cluster, OAI.HyperedgeComparison.clusters

33. theorem OAI.HyperedgeComparison.cluster_eq_of_connected line 264
34. def OAI.HyperedgeComparison.earlier line 271
35. def OAI.HyperedgeComparison.firstRoot line 274
36. theorem OAI.HyperedgeComparison.firstRoot_iff line 278
37. theorem OAI.HyperedgeComparison.exists_unique_firstRoot line 292
38. theorem OAI.HyperedgeComparison.sum_firstRoot line 315

    Source documentation

    The first-listed-node partition, as a pointwise identity for any cluster functional. This is stronger than its integrated mass identity H d = 1.

    theorem sum_firstRoot {n : ℕ} (H : Hypergraph V E) (x : Fin n → V)
        (ω : E → Bool) (D : Set V) (i : Fin n) (F : Set V → ℝ) :
        (∑ k, if firstRoot H x ω D k i then F (cluster H ω D (x k)) else 0) =
          F (cluster H ω D (x i)) := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.firstRoot, OAI.HyperedgeComparison.cluster

39. def OAI.HyperedgeComparison.law line 330
40. instance OAI.HyperedgeComparison.law_probability line 333
41. theorem OAI.HyperedgeComparison.independent_of_disjoint_bits line 339

    Source documentation

    Functions of complementary finite sets of independent bits are independent. The dependence conditions are extensional, avoiding auxiliary sigma-algebras.

    theorem independent_of_disjoint_bits (p : E → Set.Icc (0 : ℝ) 1)
        (J : Finset E) (f g : (E → Bool) → ℝ)
        (hf : ∀ ω ω', (∀ e ∈ J, ω' e = ω e) → f ω' = f ω)
        (hg : ∀ ω ω', (∀ e ∉ J, ω' e = ω e) → g ω' = g ω) :
        IndepFun f g (law p) := by
    …

    Mentions: OAI.HyperedgeComparison.law

42. theorem OAI.HyperedgeComparison.exact_cluster_independent line 367

    Source documentation

    The exact-cluster indicator sees no bit on a hyperedge disjoint from W, including when the cluster was sampled after an earlier deletion D.

    theorem exact_cluster_independent (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (D S W : Set V) (g : (E → Bool) → ℝ)
        (hg : ∀ ω ω', (∀ e, Disjoint (H e) W → ω' e = ω e) → g ω' = g ω) :
        IndepFun (fun ω => if clusters H ω D S = W then (1 : ℝ) else 0) g (law p) := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.clusters, OAI.HyperedgeComparison.law

43. theorem OAI.HyperedgeComparison.exact_cluster_integral line 398

    Source documentation

    Integrated exact-cluster independence, with no positivity restriction on an exact cluster event (zero probability events also satisfy the identity).

    theorem exact_cluster_integral (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (D S W : Set V) (g : (E → Bool) → ℝ)
        (hg : ∀ ω ω', (∀ e, Disjoint (H e) W → ω' e = ω e) → g ω' = g ω) :
        (∫ ω, (if clusters H ω D S = W then (1 : ℝ) else 0) * g ω ∂law p) =
          (∫ ω, if clusters H ω D S = W then (1 : ℝ) else 0 ∂law p) *
            ∫ ω, g ω ∂law p := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.clusters, OAI.HyperedgeComparison.law

44. theorem OAI.HyperedgeComparison.integral_eq_sum_fibers line 411

    Source documentation

    Partition a finite expectation by exact values, without conditional-probability notation and without requiring positive individual atom masses.

    theorem integral_eq_sum_fibers {I : Type uI} [Fintype I] [DecidableEq I]
        (p : E → Set.Icc (0 : ℝ) 1) (X : (E → Bool) → I) (f : (E → Bool) → ℝ) :
        (∫ ω, f ω ∂law p) = ∑ i, ∫ ω, if X ω = i then f ω else 0 ∂law p := by
    …

    Mentions: OAI.HyperedgeComparison.law

45. def OAI.HyperedgeComparison.meanAfterDelete line 420
46. def OAI.HyperedgeComparison.resample line 424
47. def OAI.HyperedgeComparison.residualMean line 428
48. theorem OAI.HyperedgeComparison.residualMean_eq_integral line 435
49. theorem OAI.HyperedgeComparison.residualMean_nonneg line 485
50. theorem OAI.HyperedgeComparison.residualMean_mono line 492
51. theorem OAI.HyperedgeComparison.meanAfterDelete_antitone line 500
52. theorem OAI.HyperedgeComparison.resample_monotone line 512
53. theorem OAI.HyperedgeComparison.resample_nonneg line 523
54. def OAI.HyperedgeComparison.clusterMass line 536
55. theorem OAI.HyperedgeComparison.cluster_conditioning line 541

    Source documentation

    The exact-cluster conditional expectation used in the column partition.

    theorem cluster_conditioning (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (s : V) (D S W : Set V) (F : Set V → ℝ)
        (hs : s ∉ W) :
        (∫ ω, if clusters H ω D S = W then F (cluster H ω D s) else 0 ∂law p) =
          clusterMass H p D S W * meanAfterDelete H p s (D ∪ W) F := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.clusters, OAI.HyperedgeComparison.cluster, OAI.HyperedgeComparison.law, OAI.HyperedgeComparison.clusterMass, OAI.HyperedgeComparison.meanAfterDelete

56. theorem OAI.HyperedgeComparison.exact_cluster_weight line 566

    Source documentation

    Multiply the exact-cluster identity by an arbitrary function of the cluster. No positive-probability conditioning is needed.

    theorem exact_cluster_weight [Fintype V] (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (D S : Set V) (f : Set V → ℝ)
        (g : (E → Bool) → Set V → ℝ)
        (hg : ∀ U ω ω', (∀ e, Disjoint (H e) U → ω' e = ω e) → g ω' U = g ω U) :
        (∫ ω, f (clusters H ω D S) * g ω (clusters H ω D S) ∂law p) =
          ∫ ω, f (clusters H ω D S) * (∫ ω', g ω' (clusters H ω D S) ∂law p) ∂law p := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.clusters, OAI.HyperedgeComparison.law

57. theorem OAI.HyperedgeComparison.conditioning_weight line 592

    Source documentation

    Exact-cluster integration of a functional rooted outside the measured cluster.

    theorem conditioning_weight [Fintype V] (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (s : V) (D S : Set V)
        (w : Set V → ℝ) (F : Set V → ℝ) (hw : ∀ U, s ∈ U → w U = 0) :
        (∫ ω, w (clusters H ω D S) * F (cluster H ω D s) ∂law p) =
          ∫ ω, w (clusters H ω D S) *
            meanAfterDelete H p s (D ∪ clusters H ω D S) F ∂law p := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.clusters, OAI.HyperedgeComparison.cluster, OAI.HyperedgeComparison.law, OAI.HyperedgeComparison.meanAfterDelete

58. theorem OAI.HyperedgeComparison.residualMean_alternative line 622

    Source documentation

    For residuals, after conditioning on W the second sample may instead be read in the original configuration on the graph with U deleted.

    theorem residualMean_alternative [Fintype V] (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (s : V) (S U : Set V) (F : Set V → ℝ) :
        residualMean H p s S U F =
          ∫ ω, if s ∈ clusters H ω U S then 0 else
            meanAfterDelete H p s (clusters H ω U S) F - F (cluster H ω U s) ∂law p := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.residualMean, OAI.HyperedgeComparison.clusters, OAI.HyperedgeComparison.meanAfterDelete, OAI.HyperedgeComparison.cluster, OAI.HyperedgeComparison.law

59. def OAI.HyperedgeComparison.column line 649
60. theorem OAI.HyperedgeComparison.sum_column line 655
61. theorem OAI.HyperedgeComparison.column_conditional_expectation line 665

    Source documentation

    The first-listed-event column disintegrates over its exact root cluster.

    theorem column_conditional_expectation [Fintype V] {n : ℕ} (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (x : Fin n → V) (k i : Fin n)
        (g : (E → Bool) → Set V → ℝ)
        (hg : ∀ U ω ω', (∀ e, Disjoint (H e) U → ω' e = ω e) → g ω' U = g ω U) :
        (∫ ω, if firstRoot H x ω ∅ k i then g ω (cluster H ω ∅ (x k)) else 0 ∂law p) =
          column H p x k (fun U => ∫ ω, g ω U ∂law p) i := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.firstRoot, OAI.HyperedgeComparison.cluster, OAI.HyperedgeComparison.law, OAI.HyperedgeComparison.column

62. theorem OAI.HyperedgeComparison.column_resample line 690
63. theorem OAI.HyperedgeComparison.earlier_mono line 711

    Source documentation

    An earlier list segment is included in every later segment.

    theorem earlier_mono {n : ℕ} (x : Fin n → V) {k j : Fin n} (hkj : k ≤ j) :
        earlier x k ⊆ earlier x j := by
    …

    Mentions: OAI.HyperedgeComparison.earlier

64. theorem OAI.HyperedgeComparison.column_residual line 718

    Source documentation

    The residual term after conditioning on C(x_j), retaining the original configuration only on hyperedges disjoint from that cluster.

    theorem column_residual [Fintype V] {n : ℕ} (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (x : Fin n → V) (k j i : Fin n)
        (hkj : k < j) (F : Set V → ℝ) :
        column H p x j (residualMean H p (x k) (earlier x k) · F) i =
          ∫ ω, if firstRoot H x ω ∅ j i ∧ x k ∉ clusters H ω ∅ (earlier x k) then
            meanAfterDelete H p (x k) (clusters H ω ∅ (earlier x k)) F -
              F (cluster H ω ∅ (x k)) else 0 ∂law p := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.column, OAI.HyperedgeComparison.residualMean, OAI.HyperedgeComparison.earlier, OAI.HyperedgeComparison.firstRoot, OAI.HyperedgeComparison.clusters, OAI.HyperedgeComparison.meanAfterDelete, OAI.HyperedgeComparison.cluster, OAI.HyperedgeComparison.law

65. theorem OAI.HyperedgeComparison.disjoint_cluster_iff_root_notin line 754

    Source documentation

    Separation from a union of full clusters is exactly avoidance by the root.

    theorem disjoint_cluster_iff_root_notin {H : Hypergraph V E} {ω : E → Bool}
        {D S : Set V} {s : V} :
        Disjoint (cluster H ω D s) S ↔ s ∉ clusters H ω D S := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.cluster, OAI.HyperedgeComparison.clusters

66. theorem OAI.HyperedgeComparison.firstRoot_notin_earlier_clusters line 766
67. theorem OAI.HyperedgeComparison.firstListed_partition line 778
68. theorem OAI.HyperedgeComparison.integral_firstListed_partition line 809

    Source documentation

    Integrated form of the first-listed-node partition.

    theorem integral_firstListed_partition {n : ℕ} (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (x : Fin n → V) (k i : Fin n)
        (g : (E → Bool) → ℝ) :
        (∫ ω, if x k ∉ clusters H ω ∅ (earlier x k) ∧ x i ∉ clusters H ω ∅ (earlier x k)
          then g ω else 0 ∂law p) =
          (∫ ω, if firstRoot H x ω ∅ k i then g ω else 0 ∂law p) +
            ∑ j, ∫ ω, if k < j ∧ firstRoot H x ω ∅ j i ∧ x k ∉ clusters H ω ∅ (earlier x k)
              then g ω else 0 ∂law p := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.clusters, OAI.HyperedgeComparison.earlier, OAI.HyperedgeComparison.law, OAI.HyperedgeComparison.firstRoot

69. theorem OAI.HyperedgeComparison.integral_indicator_sub line 822

    Source documentation

    Subtraction under a finite expectation with the same event indicator.

    theorem integral_indicator_sub (p : E → Set.Icc (0 : ℝ) 1)
        (P : (E → Bool) → Prop) [DecidablePred P] (f g : (E → Bool) → ℝ) :
        (∫ ω, if P ω then f ω - g ω else 0 ∂law p) =
          (∫ ω, if P ω then f ω else 0 ∂law p) -
            ∫ ω, if P ω then g ω else 0 ∂law p := by
    …

    Mentions: OAI.HyperedgeComparison.law

70. theorem OAI.HyperedgeComparison.column_identity line 833
71. theorem OAI.HyperedgeComparison.cluster_all_closed line 880

    Source documentation

    Closing every hyperedge isolates every node, in every deletion graph.

    theorem cluster_all_closed (H : Hypergraph V E) (D : Set V) (s : V) :
        cluster H (fun _ => false) D s = {s} := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.cluster

72. def OAI.HyperedgeComparison.nextState line 893

    Source documentation

    A state of the alternating conditional cluster resampling chain.

    noncomputable def nextState (H : Hypergraph V E) (s : V) (S : Set V)
        (U : ClusterDomain s S) (ω ω' : E → Bool) : ClusterDomain s S :=
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.ClusterDomain

73. def OAI.HyperedgeComparison.resamplingTransition line 901

    Source documentation

    The finite transition matrix for the actual two-stage cluster resampling.

    noncomputable def resamplingTransition [Fintype V] (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (s : V) (S : Set V) :
        FiniteResampling.Transition (ClusterDomain s S) where
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.FiniteResampling.Transition, OAI.HyperedgeComparison.ClusterDomain

74. theorem OAI.HyperedgeComparison.resamplingTransition_act line 918
75. theorem OAI.HyperedgeComparison.all_closed_mass line 941

    Source documentation

    Probability mass of the all-closed finite configuration.

    theorem all_closed_mass (p : E → Set.Icc (0 : ℝ) 1) :
        (law p).real {fun _ => false} = ∏ e, (1 - (p e : ℝ)) := by
    …

    Mentions: OAI.HyperedgeComparison.law

76. theorem OAI.HyperedgeComparison.all_closed_mass_pos line 951
77. theorem OAI.HyperedgeComparison.resamplingTransition_atom line 957

    Source documentation

    A uniform positive atom, without discarding any zero-mass cluster states.

    theorem resamplingTransition_atom [Fintype V] (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (s : V) (S : Set V) (hs : s ∉ S)
        (U : ClusterDomain s S) :
        (law p).real {fun _ => false} ≤ (resamplingTransition H p s S).weight U
          ⟨{s}, ⟨by simp, by simpa using hs⟩⟩ := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.ClusterDomain, OAI.HyperedgeComparison.law, OAI.HyperedgeComparison.resamplingTransition

78. theorem OAI.HyperedgeComparison.resample_tendsto_constant line 986

    Source documentation

    The actual conditional cluster-resampling iterates tend to a nonnegative constant. This version does not need stationarity or positive mass at every state.

    theorem resample_tendsto_constant [Fintype V] (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (hp : ∀ e, (p e : ℝ) < 1)
        (s : V) (S : Set V) (hs : s ∉ S) (F : Set V → ℝ)
        (hF : ∀ U ∈ ClusterDomain s S, 0 ≤ F U) :
        ∃ c : ℝ, 0 ≤ c ∧ ∀ U ∈ ClusterDomain s S,
          Tendsto (fun n : ℕ => ((resample H p s S)^[n] F) U) atTop (nhds c) := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.ClusterDomain, OAI.HyperedgeComparison.resample

79. theorem OAI.HyperedgeComparison.tendsto_integral_finite line 1017

    Source documentation

    Pointwise convergence exchanges with any expectation on a finite bit space.

    theorem tendsto_integral_finite (p : E → Set.Icc (0 : ℝ) 1)
        (f : ℕ → (E → Bool) → ℝ) (g : (E → Bool) → ℝ)
        (h : ∀ ω, Tendsto (fun n => f n ω) atTop (nhds (g ω))) :
        Tendsto (fun n => ∫ ω, f n ω ∂law p) atTop (nhds (∫ ω, g ω ∂law p)) := by
    …

    Mentions: OAI.HyperedgeComparison.law

80. theorem OAI.HyperedgeComparison.column_tendsto line 1025

    Source documentation

    Column convergence only needs convergence on its specified cluster domain.

    theorem column_tendsto {n : ℕ} (H : Hypergraph V E) (p : E → Set.Icc (0 : ℝ) 1)
        (x : Fin n → V) (k i : Fin n) (F : ℕ → Set V → ℝ) (c : ℝ)
        (h : ∀ U ∈ ClusterDomain (x k) (earlier x k),
          Tendsto (fun t => F t U) atTop (nhds c)) :
        Tendsto (fun t => column H p x k (F t) i) atTop
          (nhds (column H p x k (fun _ => c) i)) := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.ClusterDomain, OAI.HyperedgeComparison.earlier, OAI.HyperedgeComparison.column

81. def OAI.HyperedgeComparison.baseMatrix line 1041

    Source documentation

    Unnormalized cluster columns d_k h_k.

    noncomputable def baseMatrix {n : ℕ} (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (x : Fin n → V) : Matrix (Fin n) (Fin n) ℝ :=
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph

82. theorem OAI.HyperedgeComparison.root_notin_earlier line 1046
83. theorem OAI.HyperedgeComparison.baseMatrix_lowerTriangular line 1051
84. theorem OAI.HyperedgeComparison.baseMatrix_diag_pos line 1060

    Source documentation

    The diagonal mass is positive because fully closing the graph ensures E_k.

    theorem baseMatrix_diag_pos {n : ℕ} (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (hp : ∀ e, (p e : ℝ) < 1)
        (x : Fin n → V) (hx : Function.Injective x) (k : Fin n) :
        0 < baseMatrix H p x k k := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.baseMatrix

85. theorem OAI.HyperedgeComparison.baseMatrix_det_ne_zero line 1083
86. def OAI.HyperedgeComparison.coeff line 1091

    Source documentation

    Coordinates in the basis of unnormalized cluster columns.

    noncomputable def coeff {n : ℕ} (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (x : Fin n → V) (k : Fin n) (F : Set V → ℝ) : Fin n → ℝ :=
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph

87. theorem OAI.HyperedgeComparison.column_const line 1095
88. theorem OAI.HyperedgeComparison.coeff_const line 1108
89. theorem OAI.HyperedgeComparison.coeff_identity line 1124

    Source documentation

    Inverse-basis coordinates obey the same column identity.

    theorem coeff_identity [Fintype V] {n : ℕ} (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (x : Fin n → V) (k : Fin n) (F : Set V → ℝ) :
        coeff H p x k F = coeff H p x k (resample H p (x k) (earlier x k) F) +
          ∑ j, if k < j then coeff H p x j (residualMean H p (x k) (earlier x k) · F) else 0 := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.coeff, OAI.HyperedgeComparison.resample, OAI.HyperedgeComparison.earlier, OAI.HyperedgeComparison.residualMean

90. theorem OAI.HyperedgeComparison.coeff_tendsto line 1141

    Source documentation

    Convergence passes to inverse-basis coordinates by finite linearity.

    theorem coeff_tendsto {n : ℕ} (H : Hypergraph V E) (p : E → Set.Icc (0 : ℝ) 1)
        (x : Fin n → V) (k i : Fin n) (F : ℕ → Set V → ℝ) (c : ℝ)
        (h : ∀ U ∈ ClusterDomain (x k) (earlier x k),
          Tendsto (fun t => F t U) atTop (nhds c)) :
        Tendsto (fun t => coeff H p x k (F t) i) atTop
          (nhds (coeff H p x k (fun _ => c) i)) := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.ClusterDomain, OAI.HyperedgeComparison.earlier, OAI.HyperedgeComparison.coeff

91. theorem OAI.HyperedgeComparison.coeff_nonneg line 1150
92. def OAI.HyperedgeComparison.hitsOther line 1219

    Source documentation

    The observable that a cluster contains another listed vertex.

    noncomputable def hitsOther {n : ℕ} (x : Fin n → V) (k : Fin n) (U : Set V) : ℝ :=
    …

93. def OAI.HyperedgeComparison.isolatedMass line 1222
94. theorem OAI.HyperedgeComparison.isolated_firstRoot line 1227
95. theorem OAI.HyperedgeComparison.isolatedMass_pos line 1234
96. theorem OAI.HyperedgeComparison.column_hitsOther line 1260
97. theorem OAI.HyperedgeComparison.inverse_offdiag_nonpos line 1295

    Source documentation

    The inverse cluster matrix has nonpositive off-diagonal entries.

    theorem inverse_offdiag_nonpos [Fintype V] {n : ℕ} (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (hp : ∀ e, (p e : ℝ) < 1)
        (x : Fin n → V) (hx : Function.Injective x) {k i : Fin n} (hik : i ≠ k) :
        (baseMatrix H p x)⁻¹ i k ≤ 0 := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.baseMatrix

98. theorem OAI.HyperedgeComparison.baseMatrix_mulVec_one line 1326

    Source documentation

    The first-listed cluster columns partition every row.

    theorem baseMatrix_mulVec_one {n : ℕ} (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (x : Fin n → V) :
        baseMatrix H p x *ᵥ (fun _ => 1) = fun _ => 1 := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.baseMatrix

99. theorem OAI.HyperedgeComparison.inverse_mulVec_one line 1338

    Source documentation

    Consequently each row of the inverse also sums to one.

    theorem inverse_mulVec_one {n : ℕ} (H : Hypergraph V E)
        (p : E → Set.Icc (0 : ℝ) 1) (hp : ∀ e, (p e : ℝ) < 1)
        (x : Fin n → V) (hx : Function.Injective x) :
        (baseMatrix H p x)⁻¹ *ᵥ (fun _ => 1) = fun _ => 1 := by
    …

    Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.baseMatrix

100. def OAI.HyperedgeComparison.expectationVector line 1350

     Source documentation

     Expectation vector of a cluster observable at the listed vertices.

     noncomputable def expectationVector {n : ℕ} (H : Hypergraph V E)
         (p : E → Set.Icc (0 : ℝ) 1) (x : Fin n → V) (F : Set V → ℝ) : Fin n → ℝ :=
     …

     Mentions: OAI.HyperedgeComparison.Hypergraph

101. theorem OAI.HyperedgeComparison.expectationVector_eq_sum_columns line 1354
102. theorem OAI.HyperedgeComparison.inverse_expectation_nonneg line 1364

     Source documentation

     Increasing observables give nonnegative inverse expectation vectors.

     theorem inverse_expectation_nonneg [Fintype V] {n : ℕ} (H : Hypergraph V E)
         (p : E → Set.Icc (0 : ℝ) 1) (hp : ∀ e, (p e : ℝ) < 1)
         (x : Fin n → V) (hx : Function.Injective x) (F : Set V → ℝ)
         (hF0 : ∀ U, 0 ≤ F U) (hFm : Monotone F) (i : Fin n) :
         0 ≤ ((baseMatrix H p x)⁻¹ *ᵥ expectationVector H p x F) i := by
     …

     Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.baseMatrix, OAI.HyperedgeComparison.expectationVector

103. theorem OAI.HyperedgeComparison.inverse_last_diag_mul line 1376

     Source documentation

     The final diagonal entry of the inverse is reciprocal to the probability of avoiding all preceding listed vertices.

     theorem inverse_last_diag_mul {n : ℕ} (H : Hypergraph V E)
         (p : E → Set.Icc (0 : ℝ) 1) (hp : ∀ e, (p e : ℝ) < 1)
         (x : Fin (n + 1) → V) (hx : Function.Injective x) :
         (baseMatrix H p x)⁻¹ (Fin.last n) (Fin.last n) *
           baseMatrix H p x (Fin.last n) (Fin.last n) = 1 := by
     …

     Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.baseMatrix

104. theorem OAI.HyperedgeComparison.expectation_comparison line 1395

     Source documentation

     Scalar consequence of the cone: a target observable large at every earlier listed vertex must have a correspondingly large expectation at the last one.

     theorem expectation_comparison [Fintype V] {n : ℕ} (H : Hypergraph V E)
         (p : E → Set.Icc (0 : ℝ) 1) (hp : ∀ e, (p e : ℝ) < 1)
         (x : Fin (n + 1) → V) (hx : Function.Injective x) (F : Set V → ℝ)
         (hF0 : ∀ U, 0 ≤ F U) (hFm : Monotone F) (b : ℝ)
         (hb : ∀ j ≠ Fin.last n, b ≤ expectationVector H p x F j) :
         b * (1 - baseMatrix H p x (Fin.last n) (Fin.last n)) ≤
           expectationVector H p x F (Fin.last n) := by
     …

     Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.expectationVector, OAI.HyperedgeComparison.baseMatrix

105. def OAI.HyperedgeComparison.eventProb line 1437

     Source documentation

     Real probability of any event in the finite bit space.

     noncomputable def eventProb (p : E → Set.Icc (0 : ℝ) 1) (P : (E → Bool) → Prop) : ℝ :=
     …

106. theorem OAI.HyperedgeComparison.eventProb_eq_real line 1440
107. theorem OAI.HyperedgeComparison.eventProb_compl line 1445
108. def OAI.HyperedgeComparison.jointObservable line 1459

     Source documentation

     Joint cluster-hit observable, preserving both target sets.

     noncomputable def jointObservable (A T U : Set V) : ℝ :=
     …

109. theorem OAI.HyperedgeComparison.jointObservable_nonneg line 1463
110. theorem OAI.HyperedgeComparison.jointObservable_monotone line 1468
111. theorem OAI.HyperedgeComparison.expectation_jointObservable line 1478
112. theorem OAI.HyperedgeComparison.expectation_jointObservable_of_mem line 1490
113. theorem OAI.HyperedgeComparison.last_diagonal_avoidance line 1499
114. theorem OAI.HyperedgeComparison.joint_comparison_list line 1521
115. theorem OAI.HyperedgeComparison.exists_target_list line 1541
116. theorem OAI.HyperedgeComparison.joint_comparison_of_lt_one line 1580

     Source documentation

     The joint connection inequality for arbitrary finite targets, first for strictly subunit hyperedge probabilities.

     theorem joint_comparison_of_lt_one [Fintype V] (H : Hypergraph V E)
         (p : E → Set.Icc (0 : ℝ) 1) (hp : ∀ e, (p e : ℝ) < 1)
         (o : V) (A T : Set V) (b : ℝ)
         (hb : ∀ a ∈ A, b ≤ eventProb p (fun ω => Meets H ω ∅ a T)) :
         b * eventProb p (fun ω => Meets H ω ∅ o A) ≤
           eventProb p (fun ω => Meets H ω ∅ o A ∧ Meets H ω ∅ o T) := by
     …

     Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.eventProb, OAI.HyperedgeComparison.Meets

117. theorem OAI.HyperedgeComparison.law_mass line 1599

     Source documentation

     Polynomial weight of a specified finite configuration.

     theorem law_mass (p : E → Set.Icc (0 : ℝ) 1) (ω : E → Bool) :
         (law p).real {ω} = ∏ e, if ω e = true then (p e : ℝ) else 1 - (p e : ℝ) := by
     …

     Mentions: OAI.HyperedgeComparison.law

118. theorem OAI.HyperedgeComparison.eventProb_tendsto line 1611

     Source documentation

     All finite event probabilities are continuous in all parameters, including at configurations with deterministic bits.

     theorem eventProb_tendsto (p : E → Set.Icc (0 : ℝ) 1)
         (q : ℕ → E → Set.Icc (0 : ℝ) 1)
         (hq : ∀ e, Tendsto (fun n => (q n e : ℝ)) atTop (nhds (p e : ℝ)))
         (P : (E → Bool) → Prop) :
         Tendsto (fun n => eventProb (q n) P) atTop (nhds (eventProb p P)) := by
     …

     Mentions: OAI.HyperedgeComparison.eventProb

119. def OAI.HyperedgeComparison.thinParameter line 1627

     Source documentation

     Strictly subunit parameters approaching arbitrary permitted parameters.

     noncomputable def thinParameter (p : E → Set.Icc (0 : ℝ) 1) (n : ℕ) (e : E) :
         Set.Icc (0 : ℝ) 1 :=
     …

120. theorem OAI.HyperedgeComparison.thinParameter_lt_one line 1638
121. theorem OAI.HyperedgeComparison.thinParameter_tendsto line 1647
122. theorem OAI.HyperedgeComparison.joint_comparison line 1653
123. theorem OAI.HyperedgeComparison.eventProb_nonneg line 1690
124. theorem OAI.HyperedgeComparison.eventProb_le_one line 1695
125. theorem OAI.HyperedgeComparison.eventProb_mono line 1700
126. theorem OAI.HyperedgeComparison.eventProb_failure line 1709
127. theorem OAI.HyperedgeComparison.failure_comparison_mul line 1719

     Source documentation

     The strengthened hyperedge failure estimate, including all fixed-bit laws.

     theorem failure_comparison_mul [Fintype V] (H : Hypergraph V E)
         (p : E → Set.Icc (0 : ℝ) 1) (o : V) (A T : Set V) (b : ℝ)
         (hb : ∀ a ∈ A, 1 - b ≤ eventProb p (fun ω => Meets H ω ∅ a T)) :
         eventProb p (fun ω => Meets H ω ∅ o A ∧ ¬Meets H ω ∅ o T) ≤
           b * eventProb p (fun ω => Meets H ω ∅ o A) := by
     …

     Mentions: OAI.HyperedgeComparison.Hypergraph, OAI.HyperedgeComparison.eventProb, OAI.HyperedgeComparison.Meets

128. theorem OAI.HyperedgeComparison.failure_comparison line 1728
129. theorem OAI.HyperedgeComparison.joint_comparison_ennreal line 1735
130. abbrev OAI.HyperedgeComparison.Site.Node line 1758

     Source documentation

     The connector presentation uses two directed copies of each undirected edge; duplication does not change any reachable starred vertex. Nonedges are isolated connector nodes.

     abbrev Node (V : Type uV) := V ⊕ (V × V)

131. def OAI.HyperedgeComparison.Site.stars line 1760
132. def OAI.HyperedgeComparison.Site.OpenAdj line 1765
133. def OAI.HyperedgeComparison.Site.Connected line 1768
134. def OAI.HyperedgeComparison.Site.Meets line 1771
135. theorem OAI.HyperedgeComparison.Site.connected_refl line 1774
136. theorem OAI.HyperedgeComparison.Site.connected_open_right line 1777
137. theorem OAI.HyperedgeComparison.Site.connected_extend line 1784
138. theorem OAI.HyperedgeComparison.Site.connected_to_stars line 1789
139. def OAI.HyperedgeComparison.Site.Supported line 1805

     Source documentation

     Predicate propagated along a hyperedge path. It explicitly retains the site-open condition, including in the zero-edge case.

     def Supported (ω : V → Bool) (o : V) : Node V → Prop
       | Sum.inl x => Connected G ω o x
       | Sum.inr e => G.Adj e.1 e.2 ∧ (Connected G ω o e.1 ∨ Connected G ω o e.2)

     Mentions: OAI.HyperedgeComparison.Site.Node, OAI.HyperedgeComparison.Site.Connected

140. theorem OAI.HyperedgeComparison.Site.supported_label line 1809
141. theorem OAI.HyperedgeComparison.Site.supported_of_label line 1828
142. theorem OAI.HyperedgeComparison.Site.connected_of_stars line 1843
143. theorem OAI.HyperedgeComparison.Site.meets_to_stars line 1856
144. theorem OAI.HyperedgeComparison.Site.meets_of_stars line 1862
145. theorem OAI.HyperedgeComparison.Site.failure_subset_hyperedge line 1868
146. theorem OAI.HyperedgeComparison.site_failure_comparison line 1879