CopyOrbits.lean`

58 declarations, 0 contain sorry, 0 declared as axioms

Distinct subset copies under a finite group action

Copies are distinct orbit elements, not group elements or labeled embeddings. All counting and probability statements therefore retain the stabilizer multiplicities correctly, including for the empty subset.

def OAI.LeanBlast.SecondKahnKalai.copyOrbit line 29
Source documentation
The distinct copies of a finite subset under the given action.
```
def copyOrbit (F : Finset X) : Finset (Finset X) :=
…
```
abbrev OAI.LeanBlast.SecondKahnKalai.OrbitCopy line 33
Source documentation
An actual distinct copy, with no labeling multiplicity.
```
abbrev OrbitCopy (F : Finset X) := {J : Finset X // J ∈ copyOrbit G F}
```
Mentions: OAI.LeanBlast.SecondKahnKalai.copyOrbit
def OAI.LeanBlast.SecondKahnKalai.orbitCount line 36
Source documentation
The total number of distinct copies.
```
def orbitCount (F : Finset X) : ℕ := (copyOrbit G F).card
```
Mentions: OAI.LeanBlast.SecondKahnKalai.copyOrbit
def OAI.LeanBlast.SecondKahnKalai.internalCopyCount line 39
Source documentation
Copies of F whose elements all lie in the fixed set I.
```
def internalCopyCount (I F : Finset X) : ℕ :=
…
```
def OAI.LeanBlast.SecondKahnKalai.containingCopyCount line 43
Source documentation
Copies of I containing the fixed observed set U.
```
def containingCopyCount (I U : Finset X) : ℕ :=
…
```
theorem OAI.LeanBlast.SecondKahnKalai.mem_copyOrbit_iff line 46
theorem OAI.LeanBlast.SecondKahnKalai.self_mem_copyOrbit line 50
theorem OAI.LeanBlast.SecondKahnKalai.copyOrbit_nonempty line 53
theorem OAI.LeanBlast.SecondKahnKalai.orbitCount_pos line 56
instance OAI.LeanBlast.SecondKahnKalai.orbitCopy_nonempty line 59
theorem OAI.LeanBlast.SecondKahnKalai.card_OrbitCopy line 62
theorem OAI.LeanBlast.SecondKahnKalai.smul_mem_copyOrbit line 65
theorem OAI.LeanBlast.SecondKahnKalai.smul_mem_copyOrbit_iff line 70
theorem OAI.LeanBlast.SecondKahnKalai.copyOrbit_smul line 75
theorem OAI.LeanBlast.SecondKahnKalai.copyOrbit_eq_of_mem_copyOrbit line 88
theorem OAI.LeanBlast.SecondKahnKalai.card_eq_of_mem_copyOrbit line 93
def OAI.LeanBlast.SecondKahnKalai.orbitCopyEquiv line 99
Source documentation
The group acts bijectively on the set of actual orbit copies.
```
def orbitCopyEquiv (g : G) (F : Finset X) : OrbitCopy G F ≃ OrbitCopy G F where
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.OrbitCopy
theorem OAI.LeanBlast.SecondKahnKalai.orbitCopyEquiv_val line 105
theorem OAI.LeanBlast.SecondKahnKalai.internalCopyCount_le_choose line 109
Source documentation
There are no more internal copies than subsets of the correct size.
```
theorem internalCopyCount_le_choose (I F : Finset X) :
    internalCopyCount G I F ≤ Nat.choose I.card F.card := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.internalCopyCount
theorem OAI.LeanBlast.SecondKahnKalai.copyOrbit_empty line 117
theorem OAI.LeanBlast.SecondKahnKalai.orbitCount_empty line 126
theorem OAI.LeanBlast.SecondKahnKalai.internalCopyCount_empty line 129
theorem OAI.LeanBlast.SecondKahnKalai.sum_copyOrbit_smul line 134
Source documentation
Acting permutes the distinct orbit elements with no multiplicity.
```
theorem sum_copyOrbit_smul (g : G) (F : Finset X) (f : Finset X → ℕ) :
    (∑ J ∈ copyOrbit G F, f (g • J)) = ∑ J ∈ copyOrbit G F, f J := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.copyOrbit
theorem OAI.LeanBlast.SecondKahnKalai.internalCopyCount_smul line 143
theorem OAI.LeanBlast.SecondKahnKalai.containingCopyCount_smul line 149
theorem OAI.LeanBlast.SecondKahnKalai.internalCopyCount_eq_of_mem_copyOrbit line 155
theorem OAI.LeanBlast.SecondKahnKalai.containingCopyCount_eq_of_mem_copyOrbit line 160
theorem OAI.LeanBlast.SecondKahnKalai.copy_incidence_identity line 167
Source documentation
Double-count containment pairs of distinct orbit copies.
```
theorem copy_incidence_identity (I F : Finset X) :
    orbitCount G F * containingCopyCount G I F =
      orbitCount G I * internalCopyCount G I F := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.orbitCount, OAI.LeanBlast.SecondKahnKalai.containingCopyCount, OAI.LeanBlast.SecondKahnKalai.internalCopyCount
theorem OAI.LeanBlast.SecondKahnKalai.containingCopyCount_pos_iff line 190
theorem OAI.LeanBlast.SecondKahnKalai.exists_pullback_of_containingCopyCount_pos line 203
Source documentation
Positive containment can be pulled back to an actual subset of I.
```
theorem exists_pullback_of_containingCopyCount_pos {I U : Finset X}
    (hpos : 0 < containingCopyCount G I U) :
    ∃ V : Finset X, V ⊆ I ∧ U ∈ copyOrbit G V ∧ V.card = U.card := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.containingCopyCount, OAI.LeanBlast.SecondKahnKalai.copyOrbit
def OAI.LeanBlast.SecondKahnKalai.copyLaw line 212
Source documentation
The uniform law on distinct copies, rather than on labeled embeddings.
```
def copyLaw (I : Finset X) : FiniteLaw (OrbitCopy G I) :=
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.OrbitCopy
theorem OAI.LeanBlast.SecondKahnKalai.copyLaw_isPositive line 215
def OAI.LeanBlast.SecondKahnKalai.containmentProb line 219
Source documentation
Probability that a uniform actual copy contains an observed finite set.
```
def containmentProb (I U : Finset X) : ℝ :=
…
```
theorem OAI.LeanBlast.SecondKahnKalai.uniform_prob_count line 225
Source documentation
Expose the generic uniform formula with the caller's decidable predicate. The finite sets are equal extensionally even when the generic probability definition uses its own classical decision procedure.
```
private theorem uniform_prob_count (Ω : Type*) [Fintype Ω] [Nonempty Ω]
    (P : Ω → Prop) [DecidablePred P] :
    (FiniteLaw.uniform Ω).prob P = ((Finset.univ.filter P).card : ℝ) / Fintype.card Ω := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw.uniform
theorem OAI.LeanBlast.SecondKahnKalai.card_filter_OrbitCopy line 234
theorem OAI.LeanBlast.SecondKahnKalai.containmentProb_eq_count line 242
theorem OAI.LeanBlast.SecondKahnKalai.containmentProb_nonneg line 248
theorem OAI.LeanBlast.SecondKahnKalai.containmentProb_le_one line 251
theorem OAI.LeanBlast.SecondKahnKalai.containmentProb_empty line 254
theorem OAI.LeanBlast.SecondKahnKalai.containmentProb_smul line 257
theorem OAI.LeanBlast.SecondKahnKalai.containmentProb_smul_left line 261
theorem OAI.LeanBlast.SecondKahnKalai.containmentProb_smul_both line 265
theorem OAI.LeanBlast.SecondKahnKalai.containmentProb_eq_of_mem_copyOrbit line 269
theorem OAI.LeanBlast.SecondKahnKalai.containmentProb_eq_internalCopyCount line 275
Source documentation
The exact permutation-symmetry incidence identity, including the empty set.
```
theorem containmentProb_eq_internalCopyCount (I F : Finset X) :
    containmentProb G I F = (internalCopyCount G I F : ℝ) / orbitCount G F := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.containmentProb, OAI.LeanBlast.SecondKahnKalai.internalCopyCount, OAI.LeanBlast.SecondKahnKalai.orbitCount
theorem OAI.LeanBlast.SecondKahnKalai.containmentProb_copy_eq_internalCopyCount line 286
theorem OAI.LeanBlast.SecondKahnKalai.containmentProb_pos_iff line 291
theorem OAI.LeanBlast.SecondKahnKalai.exists_pullback_of_containmentProb_pos line 297
theorem OAI.LeanBlast.SecondKahnKalai.containmentProb_pos_of_copy_subset line 304
Source documentation
Every copy of a subset extends to at least one copy of its ambient set.
```
theorem containmentProb_pos_of_copy_subset {S I S₀ : Finset X}
    (hSI : S ⊆ I) (hS₀ : S₀ ∈ copyOrbit G S) : 0 < containmentProb G I S₀ := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.copyOrbit, OAI.LeanBlast.SecondKahnKalai.containmentProb
abbrev OAI.LeanBlast.SecondKahnKalai.ExtensionCopy line 312
Source documentation
Actual distinct extensions of the observed predecessor. Histories in a tree may index this same family separately; this type never merges histories.
```
abbrev ExtensionCopy (I S : Finset X) := {J : OrbitCopy G I // S ⊆ J.val}
```
Mentions: OAI.LeanBlast.SecondKahnKalai.OrbitCopy
theorem OAI.LeanBlast.SecondKahnKalai.extensionCopy_nonempty line 314
theorem OAI.LeanBlast.SecondKahnKalai.card_ExtensionCopy line 319
def OAI.LeanBlast.SecondKahnKalai.extensionLaw line 326
Source documentation
The uniform law on actual copies extending S, with positivity justified by the actual containment event.
```
def extensionLaw (I S : Finset X) (hpos : 0 < containmentProb G I S) :
    FiniteLaw (ExtensionCopy G I S) := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.containmentProb, OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.ExtensionCopy
theorem OAI.LeanBlast.SecondKahnKalai.extensionLaw_isPositive line 331
def OAI.LeanBlast.SecondKahnKalai.extensionIntersectionEquiv line 336
theorem OAI.LeanBlast.SecondKahnKalai.card_extension_filter line 344
theorem OAI.LeanBlast.SecondKahnKalai.extensionLaw_prob line 354
theorem OAI.LeanBlast.SecondKahnKalai.extensionLaw_added_prob line 375
Source documentation
For a set disjoint from the predecessor, containment in the added label is exactly the usual conditional containment event.
```
theorem extensionLaw_added_prob (I S J : Finset X) (hpos : 0 < containmentProb G I S)
    (hdis : Disjoint J S) :
    (extensionLaw G I S hpos).prob (fun C => J ⊆ C.val.val \ S) =
      containmentProb G I (S ∪ J) / containmentProb G I S := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.containmentProb, OAI.LeanBlast.SecondKahnKalai.extensionLaw
theorem OAI.LeanBlast.SecondKahnKalai.extensionLaw_added_prob_eq_zero line 382
Source documentation
A set meeting the predecessor cannot lie in any added label.
```
theorem extensionLaw_added_prob_eq_zero (I S J : Finset X)
    (hpos : 0 < containmentProb G I S) (hdis : ¬ Disjoint J S) :
    (extensionLaw G I S hpos).prob (fun C => J ⊆ C.val.val \ S) = 0 := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.containmentProb, OAI.LeanBlast.SecondKahnKalai.extensionLaw