StageExpectation.lean`

38 declarations, 0 contain sorry, 0 declared as axioms

Finite Fubini for the product of the separately girth-conditioned sides. The label set here is global: it is not replaced by the product of its two projections. This is the independence actually used in entropy.tex 396–435.

theorem OAI.TorsionFreeZeroDivisors.StageExpectation.turnProduct_bin line 20
Source documentation
The retained full-block bins bound the actual turn product of the subdivided graph, not a separate abstract word process.
```
theorem turnProduct_bin (w : C → ℤ → Letter) (d : Underlying s len → ℤ)
    (hbin : ∀ i, word s len w i ∈ binWords (height s len i) (d i)) :
    ChainRealization.turnProduct len w ≤ Real.exp (-∑ i, (d i : ℝ)) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.ChainRealization.turnProduct

theorem OAI.TorsionFreeZeroDivisors.StageExpectation.fixed_label_bin_bound line 29

Source documentation

Source equation (entropy-fixed-label-expectation), in its exact finite form before the uniform asymptotic prescription and marked-vertex errors.

theorem fixed_label_bin_bound (outgoing : TV → Finset Types.Letter)
    (pp : V → Option TV) (n p : ℝ) (hp : 0 ≤ p)
    (w : C → ℤ → Letter) (d : Underlying s len → ℤ)
    (hbin : ∀ i, word s len w i ∈ binWords (height s len i) (d i))
    (himm : Function.Injective (fun a =>
      ((graph len first last).origin a, ChainRealization.label len w a)))
    (hn : (Fintype.card TV : ℝ) ≤ n)
    (htable : ∀ t u, t ≠ u →
      (Fintype.card {x : TV // t ∈ outgoing x ∧ u ∈ outgoing x} : ℝ) ≤
        n*p*TypeWeights.jointWeight t u)
    (N D R : ℕ) (hD : 2 ≤ D) (hR : 0 < R)
    (hdegree : ∀ v, Nat.card {a : PatternEmbeddings.Dart outgoing //
…

Mentions: OAI.TorsionFreeZeroDivisors.Types.Letter, OAI.TorsionFreeZeroDivisors.ChainRealization.label, OAI.TorsionFreeZeroDivisors.TypeWeights.jointWeight, OAI.TorsionFreeZeroDivisors.PatternEmbeddings.Dart

theorem OAI.TorsionFreeZeroDivisors.StageExpectation.label_union_mean line 69

Source documentation

Finite Fubini for the actual permitted-label union. We count only immersed template labels and do not assume independence of repeated edges.

theorem label_union_mean {Ω W : Type*} (sample : Finset Ω) (labels : Finset W)
    (X : W → Ω → ℕ) (B : ℝ)
    (hX : ∀ w ∈ labels, ((∑ r ∈ sample, X w r : ℕ) : ℝ)/sample.card ≤ B) :
    ((∑ r ∈ sample, ∑ w ∈ labels, X w r : ℕ) : ℝ)/sample.card ≤
      (labels.card : ℝ)*B := by
…

def OAI.TorsionFreeZeroDivisors.StageExpectation.readWord line 81
Source documentation
Finite letters on a chain, extended only to make the integer indexing convenient. The fallback is never used at an edge of the pattern.
```
def readWord (F : ComparedBlocks.Position len → Letter) (c : C) (q : ℤ) : Letter :=
…
```
Mentions: OAI.TorsionFreeZeroDivisors.ComparedBlocks.Position
theorem OAI.TorsionFreeZeroDivisors.StageExpectation.readWord_on line 85
theorem OAI.TorsionFreeZeroDivisors.StageExpectation.word_position line 91
abbrev OAI.TorsionFreeZeroDivisors.StageExpectation.activeLen line 106
def OAI.TorsionFreeZeroDivisors.StageExpectation.activeIndex line 108
def OAI.TorsionFreeZeroDivisors.StageExpectation.activeBlockEquiv line 112
Source documentation
The active-block subtype counts exactly the full blocks of the active chains; no inactive full block is inserted into this stage.
```
def activeBlockEquiv : Underlying s (activeLen len m j) ≃ activeBlocks s len m j where
…
```
Mentions: OAI.TorsionFreeZeroDivisors.StageExpectation.activeLen
theorem OAI.TorsionFreeZeroDivisors.StageExpectation.active_bins line 122
Source documentation
A permitted full-stage assignment really has the prescribed bins on every active chain, under the literal integer coordinates.
```
theorem active_bins (cmp : Comparisons (E := E) (traversalLength len m))
…
```
theorem OAI.TorsionFreeZeroDivisors.StageExpectation.active_bin_sum line 140
Source documentation
Equality of the literal active bin sum and the filtered global bin sum.
```
theorem active_bin_sum (d : Underlying s len → ℤ) :
    (∑ i : Underlying s (activeLen len m j), (d (activeIndex s len m j i) : ℝ)) =
      ∑ i ∈ activeBlocks s len m j, (d i : ℝ) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.StageExpectation.activeLen, OAI.TorsionFreeZeroDivisors.StageExpectation.activeIndex
def OAI.TorsionFreeZeroDivisors.StageExpectation.immersedWords line 153
def OAI.TorsionFreeZeroDivisors.StageExpectation.count line 160
Source documentation
The stage random variable is a literal sum of feasible injective graph realizations, restricted to the full-word projection and to immersed labels.
```
def count (outgoing : TV → Finset Types.Letter) (pp : V → Option TV)
    (X : Finset (ComparedBlocks.Position len → Letter))
    (r : ConditionedMatchings.Matching (PatternEmbeddings.label outgoing) Types.inverse) : ℕ :=
…
```
Mentions: OAI.TorsionFreeZeroDivisors.Types.Letter, OAI.TorsionFreeZeroDivisors.ComparedBlocks.Position, OAI.TorsionFreeZeroDivisors.ConditionedMatchings.Matching, OAI.TorsionFreeZeroDivisors.PatternEmbeddings.label, OAI.TorsionFreeZeroDivisors.Types.inverse

theorem OAI.TorsionFreeZeroDivisors.StageExpectation.mean_bound line 171

Source documentation

The exact stage expectation, including the full prescribed matching model and all dependencies among repeated edge occurrences.

theorem mean_bound (outgoing : TV → Finset Types.Letter) (pp : V → Option TV)
    (X : Finset (ComparedBlocks.Position len → Letter))
    (n p : ℝ) (hp : 0 ≤ p) (d : Underlying s len → ℤ)
    (hbin : ∀ F ∈ X, ∀ i, word s len (readWord len F) i ∈
      binWords (height s len i) (d i))
    (hn : (Fintype.card TV : ℝ) ≤ n)
    (htable : ∀ t u, t ≠ u →
      (Fintype.card {x : TV // t ∈ outgoing x ∧ u ∈ outgoing x} : ℝ) ≤
        n*p*TypeWeights.jointWeight t u)
    (N D R : ℕ) (hD : 2 ≤ D) (hR : 0 < R)
    (hdegree : ∀ v, Nat.card {a : PatternEmbeddings.Dart outgoing //
      PatternEmbeddings.origin outgoing a = v} ≤ D)
…

Mentions: OAI.TorsionFreeZeroDivisors.Types.Letter, OAI.TorsionFreeZeroDivisors.ComparedBlocks.Position, OAI.TorsionFreeZeroDivisors.StageExpectation.readWord, OAI.TorsionFreeZeroDivisors.TypeWeights.jointWeight, OAI.TorsionFreeZeroDivisors.PatternEmbeddings.Dart, OAI.TorsionFreeZeroDivisors.PatternEmbeddings.origin

def OAI.TorsionFreeZeroDivisors.TwoSideMean.mean line 222
theorem OAI.TorsionFreeZeroDivisors.TwoSideMean.mean_nonneg line 224
theorem OAI.TorsionFreeZeroDivisors.TwoSideMean.mean_product line 228
theorem OAI.TorsionFreeZeroDivisors.TwoSideMean.fixed_mean_bound line 238
Source documentation
The product model factors only after a whole global label assignment is fixed. No assertion that the allowed labels on the two sides are independent.
```
theorem fixed_mean_bound (ΩA : Finset A) (ΩB : Finset B)
    (X : A → ℕ) (Y : B → ℕ) {a b : ℝ}
    (ha : mean ΩA X ≤ a) (hb : mean ΩB Y ≤ b) :
    mean (ΩA ×ˢ ΩB) (fun r => X r.1 * Y r.2) ≤ a*b := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.TwoSideMean.mean
theorem OAI.TorsionFreeZeroDivisors.TwoSideMean.label_union line 247
Source documentation
A finite union bound keeps the exact number of global label assignments, not a product of the sizes of projection sets (which could lose the entropy).
```
theorem label_union (Ω : Finset A) (labels : Finset W) (X : W → A → ℕ)
    {b : ℝ} (hX : ∀ w ∈ labels, mean Ω (X w) ≤ b) :
    mean Ω (fun r => ∑ w ∈ labels, X w r) ≤ (labels.card : ℝ)*b := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.TwoSideMean.mean
theorem OAI.TorsionFreeZeroDivisors.TwoSideMean.global_mean_bound line 256

theorem OAI.TorsionFreeZeroDivisors.TwoSideMean.filter_product line 266

Source documentation

Product conditioning is literally a product when the girth restriction is imposed separately on the disjoint sides.

theorem filter_product (ΩA : Finset A) (ΩB : Finset B) (PA : A → Prop) (PB : B → Prop) :
    (ΩA ×ˢ ΩB).filter (fun r => PA r.1 ∧ PB r.2) =
      (ΩA.filter PA) ×ˢ (ΩB.filter PB) := by
…

structure OAI.TorsionFreeZeroDivisors.TwoSideStage.Side line 283
Source documentation
A stage on one prescribed side. Its marked vertices do not include any isolated vertices of inactive chains. The source number of available vertices is n on EACH side, not the cardinality 2n of their disjoint union.
```
structure Side where
…
```
abbrev OAI.TorsionFreeZeroDivisors.TwoSideStage.Side.Word line 297
abbrev OAI.TorsionFreeZeroDivisors.TwoSideStage.Side.Match line 298
def OAI.TorsionFreeZeroDivisors.TwoSideStage.Side.samples line 300
def OAI.TorsionFreeZeroDivisors.TwoSideStage.Side.immersed line 304
def OAI.TorsionFreeZeroDivisors.TwoSideStage.Side.realizations line 308
def OAI.TorsionFreeZeroDivisors.TwoSideStage.Side.internal line 313
def OAI.TorsionFreeZeroDivisors.TwoSideStage.Side.edges line 314
def OAI.TorsionFreeZeroDivisors.TwoSideStage.Side.freeMarks line 315
def OAI.TorsionFreeZeroDivisors.TwoSideStage.Side.cost line 317
structure OAI.TorsionFreeZeroDivisors.TwoSideStage.Conditions line 322
Source documentation
All probability hypotheses are the literal finite matching conditions. No expected count or entropy estimate is a field of this certificate.
```
structure Conditions (S : Side) (n p : ℝ) (N D R : ℕ) : Prop where
…
```
Mentions: OAI.TorsionFreeZeroDivisors.TwoSideStage.Side
def OAI.TorsionFreeZeroDivisors.TwoSideStage.Side.bins line 338
theorem OAI.TorsionFreeZeroDivisors.TwoSideStage.fixed_mean line 344
Source documentation
Exact single-side specialization reused at each fixed GLOBAL label.
```
theorem fixed_mean (S : Side) (n p : ℝ) (N D R : ℕ) (h : Conditions S n p N D R)
    (F : S.Word) (hF : S.immersed F) (d : Underlying s S.len → ℤ)
    (hd : S.bins s d F) :
    TwoSideMean.mean (S.samples N) (S.realizations F) ≤
      S.cost n p R * Real.exp (-∑ i, (d i : ℝ)) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.TwoSideStage.Side, OAI.TorsionFreeZeroDivisors.TwoSideStage.Conditions, OAI.TorsionFreeZeroDivisors.TwoSideMean.mean
def OAI.TorsionFreeZeroDivisors.TwoSideStage.immersedLabels line 357
Source documentation
Only one filter of the global string set; it does not discard comparisons between sides or enlarge that set to the product of projections.
```
def immersedLabels (A B : Side) (X : Finset W) (WA : W → A.Word) (WB : W → B.Word) : Finset W :=
…
```
Mentions: OAI.TorsionFreeZeroDivisors.TwoSideStage.Side
def OAI.TorsionFreeZeroDivisors.TwoSideStage.count line 360

theorem OAI.TorsionFreeZeroDivisors.TwoSideStage.mean_bound line 367

Source documentation

Literal two-side stage first moment. Conditioning factors into the product of the girth restrictions; repeated-edge dependencies stay inside each matching.

theorem mean_bound (A B : Side) (X : Finset W) (WA : W → A.Word) (WB : W → B.Word)
    (n p : ℝ) (N D R : ℕ) (hA : Conditions A n p N D R) (hB : Conditions B n p N D R)
    (dA : Underlying s A.len → ℤ) (dB : Underlying s B.len → ℤ)
    (hdA : ∀ w ∈ X, A.bins s dA (WA w)) (hdB : ∀ w ∈ X, B.bins s dB (WB w)) :
    TwoSideMean.mean ((A.samples N) ×ˢ (B.samples N)) (count A B X WA WB) ≤
      (X.card : ℝ)*((A.cost n p R * B.cost n p R) *
        Real.exp (-(∑ i, (dA i : ℝ))-(∑ i, (dB i : ℝ)))) := by
…

Mentions: OAI.TorsionFreeZeroDivisors.TwoSideStage.Side, OAI.TorsionFreeZeroDivisors.TwoSideStage.Conditions, OAI.TorsionFreeZeroDivisors.TwoSideMean.mean, OAI.TorsionFreeZeroDivisors.TwoSideStage.count

theorem OAI.TorsionFreeZeroDivisors.TwoSideStage.cost_product line 397

Source documentation

No entropy factor 2 is introduced when the two sides are combined.

theorem cost_product (A B : Side) (n p : ℝ) (R : ℕ) :
    A.cost n p R * B.cost n p R =
      (n^(A.freeMarks+A.internal+B.freeMarks+B.internal) * p^(A.internal+B.internal)) /
        (R : ℝ)^(A.edges+B.edges) := by
…

Mentions: OAI.TorsionFreeZeroDivisors.TwoSideStage.Side