OAI/Dynamics/SmoothObstruction/PairBounds.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SmoothObstruction.FiniteLaw.expect_push_sum line 15
2. lemma OAI.SmoothObstruction.FiniteLaw.push_mass_canonical line 25

   Source documentation

   The finite push mass, independent of the choice of equality decision procedure.

   lemma push_mass_canonical [DecidableEq β] (P : Law α) (f : α → β) :
       (push P f).mass=FiniteEntropy.pushMass P.mass f := by
   …

   Mentions: OAI.SmoothObstruction.FiniteLaw.Law, OAI.SmoothObstruction.FiniteLaw.push, OAI.SmoothObstruction.FiniteEntropy.pushMass

3. lemma OAI.SmoothObstruction.FiniteLaw.mass_le_push line 34
4. lemma OAI.SmoothObstruction.FiniteLaw.entropy_mixture_upper line 44

   Source documentation

   The conditioning cost is the actual entropy of the mixing variable; zero cell masses contribute zero.

   lemma entropy_mixture_upper (P : Law α) (Q : α → Law β) :
       entropy (mixture P Q)≤entropy P+∑ a,P.mass a*entropy (Q a) := by
   …

   Mentions: OAI.SmoothObstruction.FiniteLaw.Law, OAI.SmoothObstruction.FiniteLaw.entropy, OAI.SmoothObstruction.FiniteLaw.mixture

5. lemma OAI.SmoothObstruction.FiniteLaw.entropy_card line 58
6. lemma OAI.SmoothObstruction.FiniteLaw.entropy_vector_le line 63

   Source documentation

   Entropy of a finite vector is bounded by the sum of its entry entropies. The proof works directly for any finite index type, including the empty case.

   lemma entropy_vector_le {J : Type*} [Fintype J] [DecidableEq J] (P : Law (J → α)) :
       entropy P≤∑ j,entropy (push P (fun w => w j)) := by
   …

   Mentions: OAI.SmoothObstruction.FiniteLaw.Law, OAI.SmoothObstruction.FiniteLaw.entropy, OAI.SmoothObstruction.FiniteLaw.push

7. theorem OAI.SmoothObstruction.FiniteLaw.conditional_entry_sum line 91

   Source documentation

   Finite-vector entropy after conditioning on a finite cell partition. No product assertion after mixing a shared entry index is used.

   theorem conditional_entry_sum {J : Type*} [Fintype J] [DecidableEq J]
       (P : Law α) (Q : α → Law (J → β)) :
       entropy (mixture P Q)-Real.log (Fintype.card α)≤
         ∑ a,P.mass a*∑ j,entropy (push (Q a) (fun w => w j)) := by
   …

   Mentions: OAI.SmoothObstruction.FiniteLaw.Law, OAI.SmoothObstruction.FiniteLaw.entropy, OAI.SmoothObstruction.FiniteLaw.mixture, OAI.SmoothObstruction.FiniteLaw.push

8. def OAI.SmoothObstruction.BinaryCharacter.sign line 106

   Source documentation

   The real-valued character of the two-element field.

   def sign (a : ZMod 2) : ℝ := if a = 0 then 1 else -1

9. lemma OAI.SmoothObstruction.BinaryCharacter.sign_zero line 108
10. lemma OAI.SmoothObstruction.BinaryCharacter.sign_one line 109
11. lemma OAI.SmoothObstruction.BinaryCharacter.eq_zero_or_one line 110
12. lemma OAI.SmoothObstruction.BinaryCharacter.sign_add line 113
13. lemma OAI.SmoothObstruction.BinaryCharacter.sign_neg line 121
14. lemma OAI.SmoothObstruction.BinaryCharacter.sign_sub line 124
15. lemma OAI.SmoothObstruction.BinaryCharacter.sign_sq line 126
16. lemma OAI.SmoothObstruction.BinaryCharacter.one_of_ne_zero line 129
17. lemma OAI.SmoothObstruction.BinaryCharacter.sum_sign_eq_zero line 136

    Source documentation

    Character cancellation: translation by any point where a functional is one changes every summand's sign. No probabilistic estimate is assumed.

    lemma sum_sign_eq_zero {f : V →ₗ[ZMod 2] ZMod 2}
        (hf : ∃ v, f v ≠ 0) : ∑ v, sign (f v) = 0 := by
    …

    Mentions: OAI.SmoothObstruction.BinaryCharacter.sign

18. lemma OAI.SmoothObstruction.BinaryCharacter.row_orthogonality line 148

    Source documentation

    Exact row orthogonality for the full binary bilinear character matrix.

    lemma row_orthogonality [DecidableEq V] (B : LinearMap.BilinForm (ZMod 2) V) (hB : B.Nondegenerate)
        (u w : V) :
        ∑ v, sign (B u v) * sign (B w v) = if u = w then (Fintype.card V : ℝ) else 0 := by
    …

    Mentions: OAI.SmoothObstruction.BinaryCharacter.sign

19. lemma OAI.SmoothObstruction.BinaryCharacter.column_orthogonality line 165
20. lemma OAI.SmoothObstruction.BinaryCharacter.parseval line 171

    Source documentation

    The finite Parseval identity, useful also for nonuniform light laws.

    lemma parseval (B : LinearMap.BilinForm (ZMod 2) V) (hB : B.Nondegenerate)
        (q : V → ℝ) :
        ∑ u, (∑ v, sign (B u v) * q v) ^ 2 = (Fintype.card V : ℝ) * ∑ v, q v ^ 2 := by
    …

    Mentions: OAI.SmoothObstruction.BinaryCharacter.sign

21. theorem OAI.SmoothObstruction.BinaryCharacter.bilinear_sq_le line 200

    Source documentation

    Squared spectral estimate with the exact matrix size, obtained from Parseval and the finite Cauchy--Schwarz inequality.

    theorem bilinear_sq_le (B : LinearMap.BilinForm (ZMod 2) V) (hB : B.Nondegenerate)
        (p q : V → ℝ) :
        (∑ u, ∑ v, p u * sign (B u v) * q v) ^ 2 ≤
          (Fintype.card V : ℝ) * (∑ u, p u ^ 2) * (∑ v, q v ^ 2) := by
    …

    Mentions: OAI.SmoothObstruction.BinaryCharacter.sign

22. lemma OAI.SmoothObstruction.BinaryCharacter.sign_indicator line 213
23. def OAI.SmoothObstruction.BinaryCharacter.extendZero line 221
24. lemma OAI.SmoothObstruction.BinaryCharacter.extendZero_zero line 225
25. lemma OAI.SmoothObstruction.BinaryCharacter.extendZero_coe line 228
26. lemma OAI.SmoothObstruction.BinaryCharacter.sum_remove_zero line 232
27. lemma OAI.SmoothObstruction.BinaryCharacter.nonzero_bilinear_sq_le line 238

    Source documentation

    Restricting the character matrix to nonzero indices retains the full space spectral bound, including its diagonal entries.

    lemma nonzero_bilinear_sq_le (B : LinearMap.BilinForm (ZMod 2) V) (hB : B.Nondegenerate)
        (p q : {v : V // v ≠ 0} → ℝ) :
        (∑ u : {v : V // v ≠ 0}, ∑ v : {v : V // v ≠ 0}, p u * sign (B u v) * q v) ^ 2 ≤
          (Fintype.card V : ℝ) * (∑ u, p u ^ 2) * (∑ v, q v ^ 2) := by
    …

    Mentions: OAI.SmoothObstruction.BinaryCharacter.sign

28. def OAI.SmoothObstruction.GraphBound.light line 266
29. lemma OAI.SmoothObstruction.GraphBound.light_nonneg line 270
30. lemma OAI.SmoothObstruction.GraphBound.light_le line 273
31. lemma OAI.SmoothObstruction.GraphBound.light_le_threshold line 276
32. lemma OAI.SmoothObstruction.GraphBound.sum_light_le_one line 279
33. lemma OAI.SmoothObstruction.GraphBound.sum_light_sq_le line 285
34. lemma OAI.SmoothObstruction.GraphBound.remove_heavy_pointwise line 296

    Source documentation

    Pointwise removal of all pairs with a heavy coordinate.

    lemma remove_heavy_pointwise {τ p q t : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q)
        (_ht : 0 ≤ t) (ht' : t ≤ 1) :
        p * q * t ≤ (if p ≤ τ then p else 0) * (if q ≤ τ then q else 0) * t +
          (p - if p ≤ τ then p else 0) * q + p * (q - if q ≤ τ then q else 0) := by
    …

35. def OAI.SmoothObstruction.GraphBound.passing line 303
36. theorem OAI.SmoothObstruction.GraphBound.passing_le line 308

    Source documentation

    Exactly the independent law (not a conditioned or resampled law).

    theorem passing_le {V : Type*} [AddCommGroup V] [Module (ZMod 2) V]
        (B : LinearMap.BilinForm (ZMod 2) V) (e : α → V) {p q : α → ℝ}
        (hp : ∀ i, 0 ≤ p i) (hq : ∀ i, 0 ≤ q i)
        (hpsum : ∑ i, p i = 1) (hqsum : ∑ i, q i = 1)
        {τ β : ℝ}
        (hlight : ∑ u, ∑ v, light τ p u * sign (B (e u) (e v)) * light τ q v ≤ β) :
        passing B e p q ≤ (∑ u, (p u - light τ p u)) +
          (∑ v, (q v - light τ q v)) + (1 + β) / 2 := by
    …

    Mentions: OAI.SmoothObstruction.GraphBound.light, OAI.SmoothObstruction.GraphBound.passing

37. lemma OAI.SmoothObstruction.GraphBound.light_spectral_bound line 352
38. lemma OAI.SmoothObstruction.GraphEntropy.spectral_small line 375
39. lemma OAI.SmoothObstruction.GraphEntropy.average_heavy_le line 402
40. lemma OAI.SmoothObstruction.GraphEntropy.tail_eq_heavy line 433
41. theorem OAI.SmoothObstruction.GraphEntropy.graph_independent_finite line 451

    Source documentation

    The independent graph-test bound needed in the actual cell experiment. This retains diagonal pairs and uses the original (not renormalized) input laws. The finite index includes both the cell and the coordinate of the label list.

    theorem graph_independent_finite (B : LinearMap.BilinForm (ZMod 2) V) (hB : B.Nondegenerate)
        (w : ξ → ℝ) (p q : ξ → {v : V // v ≠ 0} → ℝ)
        (hw : ∀ x, 0 ≤ w x) (hw1 : ∑ x, w x = 1)
        (hp : ∀ x i, 0 ≤ p x i) (hq : ∀ x i, 0 ≤ q x i)
        (hp1 : ∀ x, ∑ i, p x i = 1) (hq1 : ∀ x, ∑ i, q x i = 1)
        (hHp : (99 / 100 : ℝ) * Real.log (Fintype.card {v : V // v ≠ 0}) ≤
          ∑ x, w x * natEntropy (p x))
        (hHq : (99 / 100 : ℝ) * Real.log (Fintype.card {v : V // v ≠ 0}) ≤
          ∑ x, w x * natEntropy (q x))
        (hlog : 1000 * Real.log 2 ≤ Real.log (Fintype.card {v : V // v ≠ 0})) :
        ∑ x, w x * passing B Subtype.val (p x) (q x) ≤ 31 / 50 := by
    …

42. theorem OAI.SmoothObstruction.IndependentUpper.list_graph_upper line 503

    Source documentation

    The independent upper bound of source section 7 from the entropies of actual whole lists and the finite cell cost. Independence is used only conditional on the FULL index (cell,entry), never after mixing entries.

    theorem list_graph_upper (B : LinearMap.BilinForm (ZMod 2) V) (hB : B.Nondegenerate)
        (P : Law C) (U W : C → Law (J → {v : V // v≠0}))
        (hU : (249/250:ℝ)*Fintype.card J*Real.log (Fintype.card {v : V // v≠0})≤
          entropy (mixture P U))
        (hW : (249/250:ℝ)*Fintype.card J*Real.log (Fintype.card {v : V // v≠0})≤
          entropy (mixture P W))
        (hC : Real.log (Fintype.card C)≤
          (3/500:ℝ)*Fintype.card J*Real.log (Fintype.card {v : V // v≠0}))
        (hlog : 1000*Real.log 2≤Real.log (Fintype.card {v : V // v≠0})) :
        (∑ c,P.mass c*∑ j,GraphBound.passing B Subtype.val
          (push (U c) (fun w => w j)).mass (push (W c) (fun w => w j)).mass)/Fintype.card J≤31/50 := by
    …

    Mentions: OAI.SmoothObstruction.GraphBound.passing

43. theorem OAI.SmoothObstruction.PairLaw.rectangle_conditional line 564

    Source documentation

    Exact original-law finite observation formula for the weighted same-cell pair experiment. Zero-mass cells vanish without renormalizing the experiment.

    theorem rectangle_conditional (μ : Measure X) [IsProbabilityMeasure μ]
        (P : X → C) (hP : Measurable P) (U : X → A) (hU : Measurable U)
        (V : X → B) (hV : Measurable V) (a : A) (b : B) :
        (law μ P).real ((U ⁻¹' {a}) ×ˢ (V ⁻¹' {b}))=
          ∑ c,(observed μ P hP).mass c*
            (conditionalObserved μ U hU P hP c).mass a*
            (conditionalObserved μ V hV P hP c).mass b := by
    …

    Mentions: OAI.SmoothObstruction.PairLaw.law

44. theorem OAI.SmoothObstruction.PairLaw.observed_pair line 603

    Source documentation

    The full pair label law, not merely a product assertion for individual entries. It determines the single statistic used on both sides of the final contradiction.

    theorem observed_pair (μ : Measure X) [IsProbabilityMeasure μ]
        (P : X → C) (hP : Measurable P) (U : X → A) (hU : Measurable U)
        (V : X → B) (hV : Measurable V) :
        letI := law_probability μ P hP
    …

    Mentions: OAI.SmoothObstruction.PairLaw.law_probability

45. instance OAI.SmoothObstruction.PairUpper.nonzeroNonempty line 629
46. def OAI.SmoothObstruction.PairUpper.statistic line 633
47. lemma OAI.SmoothObstruction.PairUpper.product_push_expect line 638
48. lemma OAI.SmoothObstruction.PairUpper.product_statistic line 647
49. theorem OAI.SmoothObstruction.PairUpper.expectation_formula line 665

    Source documentation

    The passing statistic on the original pair law. This identifies exactly its finite expectation with source (7.2), using the full conditional lists.

    theorem expectation_formula (μ : Measure X) [IsProbabilityMeasure μ]
        (P : X → C) (hP : Measurable P)
        (U W : X → J → {v : V // v≠0}) (hU : Measurable U) (hW : Measurable W)
        (B : LinearMap.BilinForm (ZMod 2) V) :
        letI := PairLaw.law_probability μ P hP
    …

    Mentions: OAI.SmoothObstruction.PairLaw.law_probability

50. theorem OAI.SmoothObstruction.PairUpper.expectation_upper line 689

    Source documentation

    Section 7's .62 upper bound for the actual same-cell measure. The two entropy hypotheses refer to the original input probability, not the retained or renormalized measure.

    theorem expectation_upper (μ : Measure X) [IsProbabilityMeasure μ]
        (P : X → C) (hP : Measurable P)
        (U W : X → J → {v : V // v≠0}) (hU : Measurable U) (hW : Measurable W)
        (B : LinearMap.BilinForm (ZMod 2) V) (hB : B.Nondegenerate)
        (hentU : (249/250:ℝ)*Fintype.card J*Real.log (Fintype.card {v : V // v≠0})≤
          entropy (observed μ U hU))
        (hentW : (249/250:ℝ)*Fintype.card J*Real.log (Fintype.card {v : V // v≠0})≤
          entropy (observed μ W hW))
        (hC : Real.log (Fintype.card C)≤
          (3/500:ℝ)*Fintype.card J*Real.log (Fintype.card {v : V // v≠0}))
        (hlog : 1000*Real.log 2≤Real.log (Fintype.card {v : V // v≠0})) :
        letI := PairLaw.law_probability μ P hP
    …

    Mentions: OAI.SmoothObstruction.PairLaw.law_probability