OAI/Probability/TraceReconstruction/FiniteLaw.lean

GitHub source file

109 declarations, 0 contain sorry, 0 declared as axioms

FiniteLaw

Finite laws, common-reference total variation, Hellinger affinity, overlap, scalar moments, hypercontractivity, clipping, and leaf densities.

  1. structure OAI.TraceReconstruction.FiniteLaw line 18

    Source documentation

    Finite probability laws used for the exact statistical transfer.

    structure FiniteLaw (α : Type*) [Fintype α] where
…
  2. def OAI.TraceReconstruction.FiniteLaw.tv line 26
  3. def OAI.TraceReconstruction.FiniteLaw.hellingerSq line 27
  4. def OAI.TraceReconstruction.FiniteLaw.affinity line 29
  5. theorem OAI.TraceReconstruction.FiniteLaw.affinity_nonneg line 32
  6. theorem OAI.TraceReconstruction.FiniteLaw.hellingerSq_nonneg line 36
  7. theorem OAI.TraceReconstruction.FiniteLaw.hellingerSq_eq line 40
  8. theorem OAI.TraceReconstruction.FiniteLaw.affinity_le_one line 54
  9. theorem OAI.TraceReconstruction.FiniteLaw.tv_nonneg line 59
  10. theorem OAI.TraceReconstruction.FiniteLaw.tv_sq_le_hellingerSq line 61
  11. theorem OAI.TraceReconstruction.FiniteLaw.tv_le_sqrt_hellingerSq line 95
  12. def OAI.TraceReconstruction.FiniteLaw.product line 102
  13. theorem OAI.TraceReconstruction.FiniteLaw.affinity_product line 109
  14. theorem OAI.TraceReconstruction.FiniteLaw.hellingerSq_product_le line 122
  15. theorem OAI.TraceReconstruction.FiniteLaw.sqrt_sub_one_sq_le line 139
  16. theorem OAI.TraceReconstruction.FiniteLaw.hellingerSq_le_score line 147
  17. theorem OAI.TraceReconstruction.FiniteLaw.tv_product_le_sqrt_score line 172
  18. def OAI.TraceReconstruction.FiniteLaw.bind line 180
  19. theorem OAI.TraceReconstruction.FiniteLaw.tv_bind_le line 188
  20. theorem OAI.TraceReconstruction.FiniteLaw.tv_triangle line 209
  21. theorem OAI.TraceReconstruction.FiniteLaw.tv_symm line 217
  22. theorem OAI.TraceReconstruction.FiniteLaw.expectation_diff_le_tv line 223
  23. theorem OAI.TraceReconstruction.FiniteLaw.binary_testing_bound line 249
  24. theorem OAI.TraceReconstruction.FiniteLaw.sum_max_eq line 260
  25. theorem OAI.TraceReconstruction.FiniteLaw.independent_binary_testing line 274

    Source documentation

    Joint exact recovery of independent binary choices, allowing arbitrary randomized estimators. No coordinatewise decision rule is assumed.

    theorem independent_binary_testing (P Q : FiniteLaw α) (g : ℕ)
    (A : (Fin g → α) → (Fin g → Bool) → ℝ)
    (hA0 : ∀ z θ, 0 ≤ A z θ) (hA1 : ∀ z, ∑ θ, A z θ = 1) :
    (1 / (2 : ℝ) ^ g) * ∑ θ : Fin g → Bool, ∑ z : Fin g → α,
      (∏ j, (if θ j then P.mass (z j) else Q.mass (z j))) * A z θ ≤
        ((1 + tv P Q) / 2) ^ g := by
…

    Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.tv

  26. def OAI.TraceReconstruction.FiniteLaw.tensor line 308
  27. theorem OAI.TraceReconstruction.FiniteLaw.tv_tensor_le line 316
  28. theorem OAI.TraceReconstruction.FiniteLaw.tv_product_succ line 340
  29. theorem OAI.TraceReconstruction.FiniteLaw.tv_product_le line 351
  30. theorem OAI.TraceReconstruction.FiniteLaw.affinity_bind_ge line 362
  31. theorem OAI.TraceReconstruction.FiniteLaw.hellingerSq_bind_le line 390
  32. theorem OAI.TraceReconstruction.FiniteLaw.approximate_score_transfer line 397

    Source documentation

    Restoration of approximate oracle simulations before taking independent complete observations; the simulation error is charged once per sample.

    theorem approximate_score_transfer (P Q : FiniteLaw α) (K : α → FiniteLaw β)
    (R S : FiniteLaw β) (Z : α → ℝ)
    (hZ : ∀ a, Q.mass a = P.mass a * (1 + Z a)) (E : ℝ)
    (hR : tv R (P.bind K) ≤ E) (hS : tv S (Q.bind K) ≤ E) (m : ℕ) :
    tv (R.product m) (S.product m) ≤
      Real.sqrt ((m : ℝ) * ∑ a, P.mass a * Z a ^ 2) + 2 * m * E := by
…

    Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.tv

  33. def OAI.TraceReconstruction.FiniteLaw.overlap line 419
  34. theorem OAI.TraceReconstruction.FiniteLaw.overlap_eq_one_sub_tv line 421
  35. theorem OAI.TraceReconstruction.FiniteLaw.overlap_nonneg line 430
  36. def OAI.TraceReconstruction.FiniteLaw.commonPart line 435
  37. theorem OAI.TraceReconstruction.FiniteLaw.commonPart_le_left line 440
  38. def OAI.TraceReconstruction.FiniteLaw.remainderLaw line 450
  39. theorem OAI.TraceReconstruction.FiniteLaw.common_part_decomposition line 458
  40. def OAI.TraceReconstruction.FiniteLaw.prod line 490
  41. def OAI.TraceReconstruction.FiniteLaw.expect line 498
  42. theorem OAI.TraceReconstruction.FiniteLaw.expect_const line 500
  43. theorem OAI.TraceReconstruction.FiniteLaw.expect_mono line 504
  44. theorem OAI.TraceReconstruction.FiniteLaw.expect_prod line 508
  45. def OAI.TraceReconstruction.FiniteLaw.Associated line 515

    Source documentation

    Association is only used for increasing likelihood-threshold events.

    def Associated [Preorder α] (P : FiniteLaw α) : Prop :=
…

    Mentions: OAI.TraceReconstruction.FiniteLaw

  46. theorem OAI.TraceReconstruction.FiniteLaw.associated_linearOrder line 519
  47. theorem OAI.TraceReconstruction.FiniteLaw.Associated.prod line 541
  48. theorem OAI.TraceReconstruction.FiniteLaw.product_succ_expect line 559
  49. theorem OAI.TraceReconstruction.FiniteLaw.associated_product line 574
  50. theorem OAI.TraceReconstruction.FiniteLaw.density_threshold_mass line 605

    Source documentation

    An elementary Paley--Zygmund bound at threshold 1/2, for a density.

    theorem density_threshold_mass (P : FiniteLaw α) (f : α → ℝ)
    (hmean : P.expect f = 1) :
    (1 : ℝ) / 4 ≤
      (P.expect (fun a => if 1 / 2 ≤ f a then 1 else 0)) * P.expect (fun a => f a ^ 2) := by
…

    Mentions: OAI.TraceReconstruction.FiniteLaw

  51. theorem OAI.TraceReconstruction.FiniteLaw.increasing_density_overlap line 643

    Source documentation

    The common-density overlap used for consecutive pure primitive runs.

    theorem increasing_density_overlap [Preorder α] (P : FiniteLaw α) (hP : P.Associated)
    (f g : α → ℝ) (hf : ∀ a, 0 ≤ f a) (hg : ∀ a, 0 ≤ g a)
    (hfm : Monotone f) (hgm : Monotone g)
    (hf1 : P.expect f = 1) (hg1 : P.expect g = 1) :
    (1 : ℝ) / 32 ≤ P.expect (fun a => min (f a) (g a)) *
      P.expect (fun a => f a ^ 2) * P.expect (fun a => g a ^ 2) := by
…

    Mentions: OAI.TraceReconstruction.FiniteLaw

  52. def OAI.TraceReconstruction.FiniteLaw.orientedProd line 702

    Source documentation

    Orientation false uses P,Q in chronological order; true reverses them.

    def orientedProd (P Q : FiniteLaw α) (b : Bool) : FiniteLaw (α × α) :=
…

    Mentions: OAI.TraceReconstruction.FiniteLaw

  53. def OAI.TraceReconstruction.FiniteLaw.pairedHiddenMass line 705
  54. theorem OAI.TraceReconstruction.FiniteLaw.sum_pairedHiddenMass line 708
  55. theorem OAI.TraceReconstruction.FiniteLaw.pairedHiddenMass_le line 715
  56. def OAI.TraceReconstruction.FiniteLaw.pairedFlagMass line 730

    Source documentation

    None is the joint hidden flag; a visible flag reports the true orientation.

    def pairedFlagMass (P Q H : FiniteLaw α) (ω : ℝ) (b : Bool)
    (z : Option Bool × (α × α)) : ℝ :=
…

    Mentions: OAI.TraceReconstruction.FiniteLaw

  57. theorem OAI.TraceReconstruction.FiniteLaw.pairedFlagMass_nonneg line 736
  58. theorem OAI.TraceReconstruction.FiniteLaw.pairedFlagMass_sum line 747
  59. def OAI.TraceReconstruction.FiniteLaw.pairedFlagLaw line 756
  60. theorem OAI.TraceReconstruction.FiniteLaw.pairedFlag_simulation line 763

    Source documentation

    Forgetting the report recovers conditional independence for each orientation.

    theorem pairedFlag_simulation (P Q H : FiniteLaw α) (ω : ℝ) (b : Bool) (z : α × α) :
    (∑ c : Option Bool, pairedFlagMass P Q H ω b (c, z)) =
      (orientedProd P Q b).mass z := by
…

    Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.pairedFlagMass, OAI.TraceReconstruction.FiniteLaw.orientedProd

  61. theorem OAI.TraceReconstruction.FiniteLaw.pairedFlag_hidden_joint line 770

    Source documentation

    Hidden reports carry exactly zero information about the fair orientation, even after both strings have been observed.

    theorem pairedFlag_hidden_joint (P Q H : FiniteLaw α) (ω : ℝ) (b : Bool) (z : α × α) :
    (1 / 2 : ℝ) * pairedFlagMass P Q H ω b (none, z) =
      (1 / 2 : ℝ) * (ω ^ 2 * (H.prod H).mass z) := by
…

    Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.pairedFlagMass

  62. theorem OAI.TraceReconstruction.FiniteLaw.pairedFlag_hidden_probability line 776
  63. theorem OAI.TraceReconstruction.FiniteLaw.small_geometric_sum line 783
  64. theorem OAI.TraceReconstruction.FiniteLaw.small_binomial_tail line 792

    Source documentation

    Elementary tail of a binomial polynomial after cancelling orders zero and one.

    theorem small_binomial_tail (n : ℕ) {x : ℝ} (hx : 0 ≤ x) (hsmall : (n : ℝ) * x ≤ 1 / 2) :
    (∑ j ∈ Finset.range (n - 1), (n.choose (j + 2) : ℝ) * x ^ (j + 2)) ≤
      2 * ((n : ℝ) * x) ^ 2 := by
…
  65. theorem OAI.TraceReconstruction.FiniteLaw.expect_pow_expansion line 811
  66. theorem OAI.TraceReconstruction.FiniteLaw.expect_small_affine_pow line 823
  67. theorem OAI.TraceReconstruction.FiniteLaw.expect_lower_moment_le_two line 859

    Source documentation

    Only the centered first moment must vanish; lower absolute moments are obtained from the one available source moment, without boundedness.

    theorem expect_lower_moment_le_two (P : FiniteLaw α) (Z : α → ℝ) (t : ℕ)
    (ht : P.expect (fun a => |Z a| ^ t) ≤ 1) (j : ℕ) (hj : j ≤ t) :
    |P.expect (fun a => Z a ^ j)| ≤ 2 := by
…

    Mentions: OAI.TraceReconstruction.FiniteLaw

  68. theorem OAI.TraceReconstruction.FiniteLaw.expect_affine_pow_le line 883
  69. theorem OAI.TraceReconstruction.FiniteLaw.scalar_even_moment_unit line 899

    Source documentation

    Scalar two-smoothness at even moment order; its constant is linear in that order after taking the square root, as required for tensorization.

    theorem scalar_even_moment_unit (P : FiniteLaw α) (Z : α → ℝ) (k : ℕ) (hk : 1 ≤ k)
    (hcenter : P.expect Z = 0) (ht : P.expect (fun a => |Z a| ^ (2 * k)) ≤ 1) (u : ℝ) :
    P.expect (fun a => (1 + u * Z a) ^ (2 * k)) ≤
      (1 + (6 * (2 * k : ℕ) : ℝ) ^ 2 * u ^ 2) ^ k := by
…

    Mentions: OAI.TraceReconstruction.FiniteLaw

  70. theorem OAI.TraceReconstruction.FiniteLaw.scalar_even_moment line 930

    Source documentation

    Homogeneous version of the scalar even-moment inequality.

    theorem scalar_even_moment (P : FiniteLaw α) (Z : α → ℝ) (k : ℕ) (hk : 1 ≤ k)
    (hcenter : P.expect Z = 0) (ht : P.expect (fun a => |Z a| ^ (2 * k)) ≤ 1) (b v : ℝ) :
    P.expect (fun a => (b + v * Z a) ^ (2 * k)) ≤
      (b ^ 2 + (6 * (2 * k : ℕ) : ℝ) ^ 2 * v ^ 2) ^ k := by
…

    Mentions: OAI.TraceReconstruction.FiniteLaw

  71. theorem OAI.TraceReconstruction.FiniteLaw.weighted_minkowski_bound line 978
  72. theorem OAI.TraceReconstruction.FiniteLaw.product_succ_expect_tail line 1017
  73. def OAI.TraceReconstruction.multilinear line 1033
  74. def OAI.TraceReconstruction.multilinearEnergy line 1036
  75. theorem OAI.TraceReconstruction.multilinearEnergy_nonneg line 1039
  76. theorem OAI.TraceReconstruction.multilinear_cons line 1048
  77. theorem OAI.TraceReconstruction.multilinearEnergy_cons line 1064
  78. theorem OAI.TraceReconstruction.multilinear_even_moment line 1081

    Source documentation

    The finite-product moment inequality used for every score expansion. The order-cost is linear per degree, and no boundedness assumption is needed.

    theorem multilinear_even_moment {α : Type*} [Fintype α] (P : FiniteLaw α)
    (Z : α → ℝ) (k : ℕ) (hk : 1 ≤ k) (hcenter : P.expect Z = 0)
    (ht : P.expect (fun a => |Z a| ^ (2 * k)) ≤ 1)
    (n : ℕ) (A : (Fin n → Bool) → ℝ) :
    (P.product n).expect (fun x => multilinear A Z x ^ (2 * k)) ≤
      (multilinearEnergy A (6 * (2 * k : ℕ))) ^ k := by
…

    Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.multilinear, OAI.TraceReconstruction.multilinearEnergy

  79. def OAI.TraceReconstruction.monomialDegree line 1129
  80. theorem OAI.TraceReconstruction.monomial_weight line 1132
  81. theorem OAI.TraceReconstruction.multilinearEnergy_homogeneous line 1137
  82. theorem OAI.TraceReconstruction.homogeneous_even_moment line 1149
  83. def OAI.TraceReconstruction.FiniteLaw.evenMomentSq line 1161

    Source documentation

    Squared L^(2k)-norm for a finite law, expressed without measure coercions.

    def FiniteLaw.evenMomentSq {α : Type*} [Fintype α] (P : FiniteLaw α)
    (f : α → ℝ) (k : ℕ) : ℝ :=
…

    Mentions: OAI.TraceReconstruction.FiniteLaw

  84. theorem OAI.TraceReconstruction.homogeneous_moment_sq line 1165
  85. def OAI.TraceReconstruction.FiniteLaw.eventMass line 1193
  86. theorem OAI.TraceReconstruction.FiniteLaw.eventMass_nonneg line 1195
  87. theorem OAI.TraceReconstruction.FiniteLaw.eventMass_le_one line 1198
  88. def OAI.TraceReconstruction.FiniteLaw.condition line 1203
  89. theorem OAI.TraceReconstruction.FiniteLaw.overlap_condition line 1214
  90. theorem OAI.TraceReconstruction.FiniteLaw.tv_condition line 1231
  91. def OAI.TraceReconstruction.FiniteLaw.withDensity line 1238

    Source documentation

    Densities relative to one finite reference, preserving the exact normalization.

    def withDensity (P : FiniteLaw α) (f : α → ℝ) (hf : ∀ a, 0 ≤ f a)
    (hmean : P.expect f = 1) : FiniteLaw α where
…

    Mentions: OAI.TraceReconstruction.FiniteLaw

  92. theorem OAI.TraceReconstruction.FiniteLaw.density_bad_mass_sq line 1244
  93. theorem OAI.TraceReconstruction.FiniteLaw.low_density_reference_mass line 1262

    Source documentation

    Loss from the small-reference-density event by the exact available moment.

    theorem low_density_reference_mass (P : FiniteLaw α) (f : α → ℝ) (t : ℕ)
    (A : Finset α) (hA : ∀ a ∈ A, f a < 1 / 2) :
    P.eventMass A ≤ (2 : ℝ) ^ t * P.expect (fun a => |f a - 1| ^ t) := by
…

    Mentions: OAI.TraceReconstruction.FiniteLaw

  94. theorem OAI.TraceReconstruction.FiniteLaw.conditioned_density_identity line 1280

    Source documentation

    Exact common-event likelihood ratio: no lower bound is imposed off the event.

    theorem conditioned_density_identity (R : FiniteLaw α) (f g : α → ℝ)
    (hf : ∀ a, 0 ≤ f a) (hg : ∀ a, 0 ≤ g a)
    (hfm : R.expect f = 1) (hgm : R.expect g = 1)
    (A : Finset α) (hAf : ∀ a ∈ A, 0 < f a)
    (hP : 0 < (R.withDensity f hf hfm).eventMass A)
    (hQ : 0 < (R.withDensity g hg hgm).eventMass A) (a : α) :
    (condition (R.withDensity g hg hgm) A hQ).mass a =
      (condition (R.withDensity f hf hfm) A hP).mass a *
      ((R.withDensity f hf hfm).eventMass A /
        (R.withDensity g hg hgm).eventMass A * (g a / f a)) := by
…

    Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.eventMass, OAI.TraceReconstruction.FiniteLaw.condition

  95. theorem OAI.TraceReconstruction.FiniteLaw.clipped_raw_moment line 1301

    Source documentation

    The raw likelihood score on a common clipping event, at every integer moment.

    theorem clipped_raw_moment (R : FiniteLaw α) (f g : α → ℝ)
    (hf : ∀ a, 0 ≤ f a) (hfm : R.expect f = 1)
    (A : Finset α) (hAf : ∀ a ∈ A, 1 / 2 ≤ f a)
    (hP : 0 < (R.withDensity f hf hfm).eventMass A) (k : ℕ) :
    (condition (R.withDensity f hf hfm) A hP).expect
        (fun a => |g a / f a - 1| ^ (k + 1)) ≤
      (2 : ℝ) ^ k / (R.withDensity f hf hfm).eventMass A *
        R.expect (fun a => |g a - f a| ^ (k + 1)) := by
…

    Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.eventMass, OAI.TraceReconstruction.FiniteLaw.condition, OAI.TraceReconstruction.FiniteLaw.expect

  96. theorem OAI.TraceReconstruction.FiniteLaw.score_rescaling_moment line 1349

    Source documentation

    Normalizing the second conditioned law costs only its scalar normalization error.

    theorem score_rescaling_moment (P : FiniteLaw α) (u : α → ℝ)
    (c : ℝ) (hc : 0 ≤ c) (k : ℕ) :
    P.expect (fun a => |c * u a - 1| ^ (k + 1)) ≤
      2 ^ k * (c ^ (k + 1) * P.expect (fun a => |u a - 1| ^ (k + 1)) +
        |c - 1| ^ (k + 1)) := by
…

    Mentions: OAI.TraceReconstruction.FiniteLaw

  97. def OAI.TraceReconstruction.FiniteLaw.coordinateProduct line 1379
  98. def OAI.TraceReconstruction.FiniteLaw.mixture line 1384
  99. def OAI.TraceReconstruction.selectionCoefficient line 1394
  100. def OAI.TraceReconstruction.selectionDensity line 1397
  101. def OAI.TraceReconstruction.averagedCoefficient line 1400
  102. def OAI.TraceReconstruction.averagedDensity line 1403
  103. theorem OAI.TraceReconstruction.selectionDensity_expansion line 1406
  104. theorem OAI.TraceReconstruction.averagedDensity_expansion line 1416
  105. theorem OAI.TraceReconstruction.averagedDensity_difference line 1430
  106. theorem OAI.TraceReconstruction.coefficient_nonneg line 1437
  107. theorem OAI.TraceReconstruction.coefficient_le_one line 1446
  108. theorem OAI.TraceReconstruction.averagedCoefficient_empty line 1458

    Source documentation

    The coefficient for the empty subset is exactly one, before or after averaging.

    theorem averagedCoefficient_empty {n : ℕ} (R : FiniteLaw Ω) (θ : Ω → Fin n → Bool) :
    averagedCoefficient R θ (fun _ => false) = 1 := by
…

    Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.averagedCoefficient

  109. theorem OAI.TraceReconstruction.leaf_oracle_density line 1463

    Source documentation

    Exact density of the conditionally independent leaf oracle used in the source.

    theorem leaf_oracle_density [Fintype α] {n : ℕ} (P Q : FiniteLaw α) (Z : α → ℝ)
    (hscore : ∀ a, Q.mass a = P.mass a * (1 + Z a))
    (R : FiniteLaw Ω) (θ : Ω → Fin n → Bool) (x : Fin n → α) :
    (R.mixture (fun ω => FiniteLaw.coordinateProduct (fun i => if θ ω i then Q else P))).mass x =
      (∏ i, P.mass (x i)) * averagedDensity R θ Z x := by
…

    Mentions: OAI.TraceReconstruction.FiniteLaw, OAI.TraceReconstruction.FiniteLaw.coordinateProduct, OAI.TraceReconstruction.averagedDensity