OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationResourceMoments.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

Raw representation universes before prefixes or the extra prime

A raw leaf occurrence records its three actual subset choices. Products of these occurrences retain repeated weights and locally overlapping masks. Only the valid-entry universe removes overlapping local masks and deduplicates by exact weight and top mask. These are the universes counted by G, J, U.

  1. structure OAI.LowSpaceSubsetSum.RepresentationLeaf line 26
  2. abbrev OAI.LowSpaceSubsetSum.RepresentationLeaf.Occurrence line 35
  3. def OAI.LowSpaceSubsetSum.RepresentationLeaf.occurrences line 37
  4. def OAI.LowSpaceSubsetSum.RepresentationLeaf.occurrenceWeight line 40
  5. theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.occurrences_card line 44
  6. theorem OAI.LowSpaceSubsetSum.RepresentationLeaf.occurrence_subsets line 50
  7. abbrev OAI.LowSpaceSubsetSum.RepresentationUniverse.ChildOccurrence line 62
  8. abbrev OAI.LowSpaceSubsetSum.RepresentationUniverse.ParentOccurrence line 64
  9. def OAI.LowSpaceSubsetSum.RepresentationUniverse.children line 66
  10. def OAI.LowSpaceSubsetSum.RepresentationUniverse.parents line 69
  11. def OAI.LowSpaceSubsetSum.RepresentationUniverse.childWeight line 72
  12. def OAI.LowSpaceSubsetSum.RepresentationUniverse.parentWeight line 75
  13. def OAI.LowSpaceSubsetSum.RepresentationUniverse.topMask line 78
  14. def OAI.LowSpaceSubsetSum.RepresentationUniverse.localMask line 81
  15. def OAI.LowSpaceSubsetSum.RepresentationUniverse.backgroundMask line 84
  16. def OAI.LowSpaceSubsetSum.RepresentationUniverse.DisjointFour line 88

    Source documentation

    Four selections are disjoint in their natural union order.

    def DisjointFour (A B C D : Finset ι) : Prop :=
…
  17. def OAI.LowSpaceSubsetSum.RepresentationUniverse.Valid line 93

    Source documentation

    Actual validity tests reject local overlap. Top and background disjointness are automatic from the layout, and are stated here to expose the invariant.

    def Valid (x : ParentOccurrence ι) : Prop :=
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationUniverse.ParentOccurrence

  18. theorem OAI.LowSpaceSubsetSum.RepresentationUniverse.weight_four line 98
  19. theorem OAI.LowSpaceSubsetSum.RepresentationUniverse.valid_weight line 103
  20. def OAI.LowSpaceSubsetSum.RepresentationUniverse.entry line 111
  21. def OAI.LowSpaceSubsetSum.RepresentationUniverse.validEntries line 114
  22. theorem OAI.LowSpaceSubsetSum.RepresentationUniverse.children_card line 120
  23. theorem OAI.LowSpaceSubsetSum.RepresentationUniverse.parents_card line 126
  24. def OAI.LowSpaceSubsetSum.RepresentationUniverse.entryFromParts line 132

    Source documentation

    The counting target has one key per top mask, background subset and local distinct weight, independent of the number of raw representations.

    def entryFromParts (a : ι → ℤ) (x : (Finset ι × Finset ι) × ℤ) : Entry ι :=
…

    Mentions: OAI.LowSpaceSubsetSum.Entry

  25. def OAI.LowSpaceSubsetSum.RepresentationUniverse.entryEnvelope line 135
  26. theorem OAI.LowSpaceSubsetSum.RepresentationUniverse.entryEnvelope_card line 139
  27. theorem OAI.LowSpaceSubsetSum.RepresentationUniverse.validEntries_card line 145
  28. theorem OAI.LowSpaceSubsetSum.RepresentationUniverse.mem_parents line 171
  29. def OAI.LowSpaceSubsetSum.RepresentationUniverse.topDomain line 176
  30. def OAI.LowSpaceSubsetSum.RepresentationUniverse.mixerDomain line 179
  31. def OAI.LowSpaceSubsetSum.RepresentationUniverse.backgroundDomain line 182
  32. theorem OAI.LowSpaceSubsetSum.RepresentationUniverse.parent_part_subsets line 186
  33. theorem OAI.LowSpaceSubsetSum.RepresentationUniverse.topMask_card line 203
  34. theorem OAI.LowSpaceSubsetSum.RepresentationUniverse.concrete_validEntries_card line 224

    Source documentation

    No entry-count premise: this follows directly from leaf domains and choices.

    theorem concrete_validEntries_card (a : ι → ℤ) (L : Fin 4 → RepresentationLeaf ι)
    (ht : DisjointFour (L 0).top (L 1).top (L 2).top (L 3).top) :
    (validEntries a L).card ≤
      (topDomain L).card.choose ((L 0).topCount + (L 1).topCount +
        (L 2).topCount + (L 3).topCount) * 2 ^ (backgroundDomain L).card *
          distinctSumCount a (mixerDomain L) :=
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationLeaf, OAI.LowSpaceSubsetSum.RepresentationUniverse.DisjointFour, OAI.LowSpaceSubsetSum.RepresentationUniverse.validEntries, OAI.LowSpaceSubsetSum.RepresentationUniverse.topDomain, OAI.LowSpaceSubsetSum.RepresentationUniverse.backgroundDomain, OAI.LowSpaceSubsetSum.distinctSumCount, OAI.LowSpaceSubsetSum.RepresentationUniverse.mixerDomain

  35. def OAI.LowSpaceSubsetSum.RepresentationMoments.mean line 241
  36. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.mean_add line 244
  37. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.mean_const line 248
  38. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.mean_prod line 253
  39. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.mean_equiv line 258
  40. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.mean_residue line 264
  41. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.mean_residue_complement line 268
  42. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.mean_two_residues line 275
  43. abbrev OAI.LowSpaceSubsetSum.RepresentationMoments.Residues line 284
  44. def OAI.LowSpaceSubsetSum.RepresentationMoments.G line 286
  45. def OAI.LowSpaceSubsetSum.RepresentationMoments.JL line 299
  46. def OAI.LowSpaceSubsetSum.RepresentationMoments.JR line 305
  47. def OAI.LowSpaceSubsetSum.RepresentationMoments.UL line 312
  48. def OAI.LowSpaceSubsetSum.RepresentationMoments.UR line 316
  49. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.mean_G line 324

    Source documentation

    All four child residues have the stated marginal laws, including the two complementary residues depending on the independently chosen parent residue.

    theorem mean_G (a : ι → ℤ) (L R : Fin 4 → RepresentationLeaf ι) (t : ℤ) :
    mean (fun r : Residues p0 pL pR => (G hL hR a L R t r : ℝ)) =
      ((RepresentationUniverse.children L 0).card + (RepresentationUniverse.children L 1).card : ℝ) / pL +
      ((RepresentationUniverse.children R 0).card + (RepresentationUniverse.children R 1).card : ℝ) / pR := by
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationLeaf, OAI.LowSpaceSubsetSum.RepresentationMoments.mean, OAI.LowSpaceSubsetSum.RepresentationMoments.Residues, OAI.LowSpaceSubsetSum.RepresentationMoments.G, OAI.LowSpaceSubsetSum.RepresentationUniverse.children

  50. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.mean_JL line 339
  51. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.mean_JR line 353
  52. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.mean_UL line 373
  53. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.mean_UR line 383
  54. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.count_tail line 394
  55. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.scale_ratio line 402
  56. def OAI.LowSpaceSubsetSum.RepresentationMoments.GoodResource line 411

    Source documentation

    The resource event is determined before the extra prime, prefixes, or separating families. Counts are taken on raw occurrences or actual entry keys.

    def GoodResource (a : ι → ℤ) (L R : Fin 4 → RepresentationLeaf ι) (t : ℤ)
    (u gamma lambda halfN : ℝ) (r : Residues p0 pL pR) : Prop :=
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationLeaf, OAI.LowSpaceSubsetSum.RepresentationMoments.Residues

  57. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.resource_failure_le line 420

    Source documentation

    The hypotheses are deterministic finite universe bounds, not moment or trial-success assumptions. The moments themselves are the exact identities above.

    theorem resource_failure_le (a : ι → ℤ) (L R : Fin 4 → RepresentationLeaf ι) (t : ℤ)
    (u gamma lambda halfN : ℝ) (hu : 0 < u)
    (hG : ((RepresentationUniverse.children L 0).card + (RepresentationUniverse.children L 1).card : ℝ) / pL +
      ((RepresentationUniverse.children R 0).card + (RepresentationUniverse.children R 1).card : ℝ) / pR ≤
        u ^ 26 * (2 : ℝ) ^ gamma)
    (hJ : ((RepresentationUniverse.parents L).card : ℝ) / (p0 * pL : ℕ) +
      ((RepresentationUniverse.parents R).card : ℝ) / (p0 * pR : ℕ) ≤
        u ^ 51 * (2 : ℝ) ^ halfN)
    (hUL : ((RepresentationUniverse.validEntries a L).card : ℝ) / p0 ≤
      u ^ 10 * (2 : ℝ) ^ lambda)
    (hUR : ((RepresentationUniverse.validEntries a R).card : ℝ) / p0 ≤
      u ^ 10 * (2 : ℝ) ^ lambda) :
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationLeaf, OAI.LowSpaceSubsetSum.RepresentationUniverse.children, OAI.LowSpaceSubsetSum.RepresentationUniverse.parents, OAI.LowSpaceSubsetSum.RepresentationUniverse.validEntries

  58. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.reciprocal_pow_small line 479
  59. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.resource_failure_small line 492
  60. theorem OAI.LowSpaceSubsetSum.RepresentationMoments.joint_failure_average line 513

    Source documentation

    Averaging conditional failure bounds preserves a joint bound with the passing event. No conditioning on the rare survival event is performed.

    theorem joint_failure_average {Ω : Type*} [Fintype Ω] (μ : FiniteLaw Ω)
    (Ψ : Ω → Type*) [∀ x, Fintype (Ψ x)] [∀ x, Nonempty (Ψ x)]
    (passing : Ω → Prop) (bad : ∀ x, Ψ x → Prop) {delta : ℝ} (hd : 0 ≤ delta)
    (hb : ∀ x, passing x → finiteUniformProbability (bad x) ≤ delta) :
    (μ.bind Ψ (fun _ => FiniteLaw.uniform)).probability
      (fun x => passing x.1 ∧ bad x.1 x.2) ≤ delta := by
…

    Mentions: OAI.LowSpaceSubsetSum.FiniteLaw, OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.FiniteLaw.uniform

  61. def OAI.LowSpaceSubsetSum.RepresentationSetup.rawPartitionBlock line 539

    Source documentation

    The exact labeled block supplied by the sampled partition.

    noncomputable def rawPartitionBlock (z : Layout n) (f : R.Partitions z)
    (j : Fin 3) (a : ℕ) : Finset (Fin n) :=
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout

  62. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawPartitionBlock_subset line 544
  63. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawPartitionBlock_disjoint line 547
  64. def OAI.LowSpaceSubsetSum.RepresentationSetup.rawBackground line 559

    Source documentation

    Eight disjoint background allocations in a fixed order. This uses all outside indices, regardless of which ones belong to the fixed solution.

    def rawBackground (z : Layout n) (B : Fin n → Fin 2 × Fin 4)
    (j : Fin 2) (i : Fin 4) : Finset (Fin n) :=
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout

  65. def OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf line 564

    Source documentation

    Table 1's actual leaf domains and rounded prescribed counts.

    noncomputable def rawLeaf (z : Layout n) (g : Guesses n) (f : R.Partitions z)
    (B : Fin n → Fin 2 × Fin 4) (j : Fin 2) (i : Fin 4) : RepresentationLeaf (Fin n) where
…

    Mentions: OAI.LowSpaceSubsetSum.RepresentationSetup.Layout, OAI.LowSpaceSubsetSum.RepresentationSetup.Guesses, OAI.LowSpaceSubsetSum.RepresentationLeaf

  66. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_top_disjoint line 574
  67. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.rawLeaf_validEntries_card line 591