A5ReverseIndex.lean`

51 declarations, 0 contain sorry, 0 declared as axioms

Pointwise identification of the natural frequency transport with the relative frequency used by the actual reverse compression fibers.

abbrev OAI.MaxCutGames.Appendix.A5ReverseIndex.EarlierA line 18
Source documentation
Earlier codomain constraints inside the final codomain constraint.
```
abbrev EarlierA (A' : Submodule F2 V) (i : ℕ) :=
…
```
abbrev OAI.MaxCutGames.Appendix.A5ReverseIndex.EarlierB line 22
Source documentation
Earlier retained domains containing the final retained domain.
```
abbrev EarlierB (B' : Submodule F2 W) (j : ℕ) :=
…
```

def OAI.MaxCutGames.Appendix.A5ReverseIndex.frequencyEquiv line 27

Source documentation

Natural frequency coordinates for an earlier pair inside a fixed final pair. This is a change of domain and codomain separately.

def frequencyEquiv (A A' : Submodule F2 V) (B' B : Submodule F2 W)
    (hA : A ≤ A') (hB : B' ≤ B) :
    (B' →ₗ[F2] (V ⧸ A')) ≃ₗ[F2]
      ((B'.comap B.subtype) →ₗ[F2] ((V ⧸ A) ⧸ A'.map A.mkQ)) :=
…

def OAI.MaxCutGames.Appendix.A5ReverseIndex.relativeFrequency line 35
theorem OAI.MaxCutGames.Appendix.A5ReverseIndex.relativeFrequency_rank line 39
abbrev OAI.MaxCutGames.Appendix.A5ReverseIndex.Ancestor line 49
Source documentation
The exact reverse fiber after the earlier dimensions are fixed.
```
abbrev Ancestor (A' : Submodule F2 V) (B' : Submodule F2 W)
    (Y : B' →ₗ[F2] (V ⧸ A')) (i j : ℕ) :=
…
```
theorem OAI.MaxCutGames.Appendix.A5ReverseIndex.relative_codomain_dimension line 57
theorem OAI.MaxCutGames.Appendix.A5ReverseIndex.relative_domain_codimension_le line 66

theorem OAI.MaxCutGames.Appendix.A5ReverseIndex.card_local_antecedent_le line 77

Source documentation

Each fixed earlier pair contributes at most two graph-parameter budgets.

theorem card_local_antecedent_le (A A' : Submodule F2 V)
    (B' B : Submodule F2 W) (hA : A ≤ A') (hB : B' ≤ B)
    (Y : B' →ₗ[F2] (V ⧸ A')) (d k : ℕ)
    (hY : Module.finrank F2 Y.range ≤ k)
    (hAd : Module.finrank F2 A' ≤ d)
    (hBd : Module.finrank F2 (W ⧸ B') ≤ d) :
    Nat.card (AntecedentCount.Antecedent
      (B'.comap B.subtype) (A'.map A.mkQ)
      (relativeFrequency A A' B' B hA hB Y)) ≤ 2 ^ (2 * d * k) := by
…

Mentions: OAI.MaxCutGames.Appendix.AntecedentCount.Antecedent, OAI.MaxCutGames.Appendix.A5ReverseIndex.relativeFrequency

theorem OAI.MaxCutGames.Appendix.A5ReverseIndex.card_sigma_le_inline_A5ReverseIndex line 101

theorem OAI.MaxCutGames.Appendix.A5ReverseIndex.card_ancestor_le line 114

Source documentation

Sharp graph-based upper bound for the entire actual reverse fiber.

theorem card_ancestor_le (A' : Submodule F2 V) (B' : Submodule F2 W)
    (Y : B' →ₗ[F2] (V ⧸ A')) (d i j k : ℕ)
    (hY : Module.finrank F2 Y.range ≤ k)
    (hA : Module.finrank F2 A' ≤ d)
    (hB : Module.finrank F2 (W ⧸ B') ≤ d) :
    Nat.card (Ancestor A' B' Y i j) ≤ 2 ^ (d * (i + j) + 2 * d * k) := by
…

Mentions: OAI.MaxCutGames.Appendix.A5ReverseIndex.Ancestor

theorem OAI.MaxCutGames.Appendix.A5ReverseIndex.card_ancestor_le_source line 143
theorem OAI.MaxCutGames.Appendix.A5FrequencyTransport.quotient_relativeFrequency_apply line 174
theorem OAI.MaxCutGames.Appendix.A5FrequencyTransport.quotient_compress_apply line 186

theorem OAI.MaxCutGames.Appendix.A5FrequencyTransport.compression_eq_relativeFrequency_of_pointwise line 195

Source documentation

The relative compression equation follows from the concrete map to the direct quotient on each element of the retained subspace.

theorem compression_eq_relativeFrequency_of_pointwise
    (A A' : Submodule F2 V) (B' B : Submodule F2 W)
    (hA : A ≤ A') (hB : B' ≤ B)
    (X : B →ₗ[F2] (V ⧸ A)) (Y : B' →ₗ[F2] (V ⧸ A'))
    (hY : ∀ b : B', Submodule.mapQ A A' LinearMap.id hA
      (X ⟨b.val, hB b.property⟩) = Y b) :
    compress X (A'.map A.mkQ) (B'.comap B.subtype) =
      A5ReverseIndex.relativeFrequency A A' B' B hA hB Y := by
…

Mentions: OAI.MaxCutGames.Appendix.A5ReverseIndex.relativeFrequency

theorem OAI.MaxCutGames.Appendix.A5FrequencyTransport.quotientFactor_mapQ line 212
theorem OAI.MaxCutGames.Appendix.A5FrequencyTransport.dualFactor_quotient line 222
theorem OAI.MaxCutGames.Appendix.A5FrequencyTransport.outputFactor_symm_as_inclusion line 233

theorem OAI.MaxCutGames.Appendix.A5FrequencyTransport.compression_eq_relativeFrequency_dualFactor line 245

Source documentation

The naturally transported local compression belongs to the precise relative-frequency fiber used in A5ReverseIndex.Ancestor.

theorem compression_eq_relativeFrequency_dualFactor
    (A : Submodule F2 V) (B : Submodule F2 W)
    (C : Submodule F2 (V ⧸ A)) (D : Submodule F2 B)
    (hA : A ≤ C.comap A.mkQ) (hB : D.map B.subtype ≤ B)
    (X : B →ₗ[F2] (V ⧸ A)) :
    compress X ((C.comap A.mkQ).map A.mkQ) ((D.map B.subtype).comap B.subtype) =
      A5ReverseIndex.relativeFrequency A (C.comap A.mkQ) (D.map B.subtype) B hA hB
        (dualFactor A B C D (compress X C D)) := by
…

Mentions: OAI.MaxCutGames.Appendix.A5ReverseIndex.relativeFrequency

theorem OAI.MaxCutGames.Appendix.A5FrequencyTransport.isAntecedent_relativeFrequency_dualFactor line 264

Source documentation

Package the actual naturally transported label into its counted antecedent fiber, retaining the original map as the witness.

theorem isAntecedent_relativeFrequency_dualFactor
    (A : Submodule F2 V) (B : Submodule F2 W)
    (C : Submodule F2 (V ⧸ A)) (D : Submodule F2 B)
    (hA : A ≤ C.comap A.mkQ) (hB : D.map B.subtype ≤ B)
    (X : B →ₗ[F2] (V ⧸ A))
    (hdis : Disjoint X.range C) (hcover : D ⊔ X.ker = ⊤) :
    AntecedentCount.IsAntecedent ((D.map B.subtype).comap B.subtype)
      ((C.comap A.mkQ).map A.mkQ)
      (A5ReverseIndex.relativeFrequency A (C.comap A.mkQ) (D.map B.subtype) B hA hB
        (dualFactor A B C D (compress X C D))) X := by
…

Mentions: OAI.MaxCutGames.Appendix.AntecedentCount.IsAntecedent, OAI.MaxCutGames.Appendix.A5ReverseIndex.relativeFrequency

abbrev OAI.MaxCutGames.Appendix.A5ForwardIndex.Index line 295
def OAI.MaxCutGames.Appendix.A5ForwardIndex.descendant line 299
def OAI.MaxCutGames.Appendix.A5ForwardIndex.sourceI line 305
def OAI.MaxCutGames.Appendix.A5ForwardIndex.sourceJ line 308
def OAI.MaxCutGames.Appendix.A5ForwardIndex.targetRank line 311
theorem OAI.MaxCutGames.Appendix.A5ForwardIndex.descendant_rank line 315
theorem OAI.MaxCutGames.Appendix.A5ForwardIndex.original_size line 320
theorem OAI.MaxCutGames.Appendix.A5ForwardIndex.original_order_bounds line 326
theorem OAI.MaxCutGames.Appendix.A5ForwardIndex.descendant_size_le line 333
theorem OAI.MaxCutGames.Appendix.A5ForwardIndex.earlierA_le line 339
theorem OAI.MaxCutGames.Appendix.A5ForwardIndex.earlierB_le line 347
abbrev OAI.MaxCutGames.Appendix.A5ForwardIndex.Fiber line 352
def OAI.MaxCutGames.Appendix.A5ForwardIndex.encode line 357
Source documentation
The encoder keeps the actual earlier pair and actual earlier map.
```
def encode (d : ℕ) (r : A13Index.Triple (E := E) (F := F)) (i j : ℕ)
…
```
Mentions: OAI.MaxCutGames.Appendix.A13Index.Triple
def OAI.MaxCutGames.Appendix.A5ForwardIndex.earlierTriple line 368
theorem OAI.MaxCutGames.Appendix.A5ForwardIndex.earlierTriple_encode line 374
theorem OAI.MaxCutGames.Appendix.A5ForwardIndex.encode_injective line 384
Source documentation
Fixing the result and retained earlier data fixes both the complementary pair and its outer hybrid index. No additional outer-index factor occurs.
```
theorem encode_injective (d : ℕ)
    (r : A13Index.Triple (E := E) (F := F)) (i j : ℕ) :
…
```
Mentions: OAI.MaxCutGames.Appendix.A13Index.Triple
theorem OAI.MaxCutGames.Appendix.A5ForwardIndex.card_fiber_le line 414
Source documentation
Actual cardinality bound for every fiber used by the weighted reversal.
```
theorem card_fiber_le (d : ℕ) (r : A13Index.Triple (E := E) (F := F)) (i j : ℕ) :
…
```
Mentions: OAI.MaxCutGames.Appendix.A13Index.Triple
theorem OAI.MaxCutGames.Appendix.A5WeightedReindex.exponent_weight_le line 445
theorem OAI.MaxCutGames.Appendix.A5WeightedReindex.counted_weight_le line 460
def OAI.MaxCutGames.Appendix.A5WeightedReindex.fiber line 477

theorem OAI.MaxCutGames.Appendix.A5WeightedReindex.sum_grouped line 481

Source documentation

Exact finite grouping by the actual result and both dimension indices.

theorem sum_grouped (d : ℕ) (result : α → β) (i j : α → ℕ)
    (hbound : ∀ a, i a ≤ d ∧ j a ≤ d) (C : β → ℕ → ℕ → ℝ) :
    (∑ a, C (result a) (i a) (j a)) =
      ∑ b, ∑ r ∈ Finset.range (d + 1), ∑ s ∈ Finset.range (d + 1),
        ((fiber result i j b r s).card : ℝ) * C b r s := by
…

Mentions: OAI.MaxCutGames.Appendix.A5WeightedReindex.fiber

theorem OAI.MaxCutGames.Appendix.A5WeightedReindex.weighted_reindex line 501
def OAI.MaxCutGames.Appendix.A5ReverseSum.actualMoment line 616
def OAI.MaxCutGames.Appendix.A5ReverseSum.targetWeight line 620
theorem OAI.MaxCutGames.Appendix.A5ReverseSum.targetWeight_nonneg line 625
theorem OAI.MaxCutGames.Appendix.A5ReverseSum.targetWeight_descendant line 632
theorem OAI.MaxCutGames.Appendix.A5ReverseSum.sum_triples_cutoff line 643
Source documentation
The target cutoff is exactly the actual finite hybrid index.
```
theorem sum_triples_cutoff (d : ℕ)
    (H : ∀ (A : Submodule F2 E) (B : Submodule F2 F),
      (B →ₗ[F2] (E ⧸ A)) → ℝ) :
    (∑ r : A13Index.Triple (E := E) (F := F),
…
```
Mentions: OAI.MaxCutGames.Appendix.A13Index.Triple
theorem OAI.MaxCutGames.Appendix.A5ReverseSum.target_sum_eq line 674
theorem OAI.MaxCutGames.Appendix.A5ReverseSum.source_summand_eq line 705
theorem OAI.MaxCutGames.Appendix.A5ReverseSum.source_sum_eq line 715
theorem OAI.MaxCutGames.Appendix.A5ReverseSum.weighted_descendantSum_le line 736
Source documentation
The weighted sum of actual A.5 descendants is bounded by damped actual map-derivative moments over all hybrid restrictions of order at most d.
```
theorem weighted_descendantSum_le (d : ℕ) (hd : 1 ≤ d)
    (f : (E →ₗ[F2] F) → ℝ) :
    (∑ r : A13Index.BoundedPositiveTriple (E := E) (F := F) d,
…
```
Mentions: OAI.MaxCutGames.Appendix.A13Index.BoundedPositiveTriple