OAI/Algebra/GroupRing/StageEntropy.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.StageEntropy.labelCost line 18

   Source documentation

   The literal label/bin exponent, in the stage bound.

   def labelCost (j : ℕ) : ℝ :=
   …

2. theorem OAI.TorsionFreeZeroDivisors.StageEntropy.labelCost_eq line 24
3. def OAI.TorsionFreeZeroDivisors.StageEntropy.looseCost line 42

   Source documentation

   The source uniform block-propagation and chain-tail error, before taking limits. All blocks and both sides are counted only once.

   def looseCost : ℝ :=
   …

4. theorem OAI.TorsionFreeZeroDivisors.StageEntropy.sum_exponents line 49

   Source documentation

   Literal component costs dispatched through proven unmatched-incidence and layer-cake estimates. The power hypothesis is the (separate) actual immersed-path vertex/edge inequality, not a first-moment assumption.

   theorem sum_exponents (M : ℕ) (hm : ∀ c, m c ≤ M) (a logn : ℝ)
       (power error : Fin M → ℝ) (ha : 0≤a) (hn : 0≤logn)
       (hlow : ∀ i, (1/600:ℝ)*s/2 ≤ d i) (hhigh : ∀ i, (d i : ℝ) ≤ a*s)
       (hpower : ∑ j, power j ≤ 0) :
       (Finset.univ.sum (fun j : Fin M => power j*logn + labelCost s hs len m cmp err d j.val + error j)) ≤
         a*s*Fintype.card (ActualStageLabels.P s hs len m cmp err).Unmatched -
           (1/1200:ℝ)*s*(∑ i : Underlying s len, (multiplicity s len m i : ℝ)) +
             ∑ j : Fin M, error j := by
   …

   Mentions: OAI.TorsionFreeZeroDivisors.StageEntropy.labelCost, OAI.TorsionFreeZeroDivisors.ActualStageLabels.P

5. theorem OAI.TorsionFreeZeroDivisors.StageEntropy.mean_bound line 82

   Source documentation

   A complete literal-stage first moment, with its signed vertex exponent and the source denominator, without stage independence.

   theorem mean_bound (cmp : Comparisons (E := E) (traversalLength len m))
   …

6. def OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.transportUnmatched line 123
7. theorem OAI.TorsionFreeZeroDivisors.OccurrenceMatching.Data.card_unmatched line 133
8. def OAI.TorsionFreeZeroDivisors.StageMass.totalLength line 147
9. def OAI.TorsionFreeZeroDivisors.StageMass.uncovered line 148
10. theorem OAI.TorsionFreeZeroDivisors.StageMass.unmatched_card line 150
11. theorem OAI.TorsionFreeZeroDivisors.StageMass.unmatched_bound line 159

    Source documentation

    The occurrence involution used by the entropy components has exactly the unmatched mass of the literal half-integer comparisons.

    theorem unmatched_bound (ν : E → ℤ) (hsmall : 2*(err:ℝ)<s-1)
        (herr : ∀ e,2*|(cmp.offset e:ℝ)-(ν e:ℝ)*s|+4≤err) :
        s*Fintype.card (ActualStageLabels.P s hs len m cmp err).Unmatched ≤
          uncovered s hs len m cmp err + 22*s*Fintype.card E + totalLength len m/s := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ActualStageLabels.P, OAI.TorsionFreeZeroDivisors.StageMass.uncovered, OAI.TorsionFreeZeroDivisors.StageMass.totalLength

12. theorem OAI.TorsionFreeZeroDivisors.StageMass.totalLength_eq line 168

    Source documentation

    Repeated traversal length is counted with its actual multiplicity.

    theorem totalLength_eq : totalLength len m = ∑ c, (m c:ℝ)*len c := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.StageMass.totalLength

13. theorem OAI.TorsionFreeZeroDivisors.StageMass.fullMass_eq line 173
14. theorem OAI.TorsionFreeZeroDivisors.StageMass.fullMass_lower line 182

    Source documentation

    The only mass lost from full blocks is at the ends of actual chain traversals. In particular repeated paths do not reduce this loss count.

    theorem fullMass_lower : totalLength len m ≤
        s*(∑ i : Underlying s len, (multiplicity s len m i:ℝ)) + s*(∑ c,(m c:ℝ)) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.StageMass.totalLength

15. theorem OAI.TorsionFreeZeroDivisors.StageMass.fullMass_lower_bounded line 192
16. def OAI.TorsionFreeZeroDivisors.StageMass.residual line 211
17. theorem OAI.TorsionFreeZeroDivisors.StageMass.exponent_sum_bound line 216

    Source documentation

    All explicit finite stage losses, before the common-scale limit.

    theorem exponent_sum_bound (M Q : ℕ) (hm : ∀ c,m c≤M) (hQ : Fintype.card C≤Q)
        (ν : E → ℤ) (hsmall : 2*(err:ℝ)<s-1)
        (herr : ∀ e,2*|(cmp.offset e:ℝ)-(ν e:ℝ)*s|+4≤err)
        (d : Underlying s len → ℤ) (hlow : ∀ i,(1/600:ℝ)*s/2≤d i)
        (hhigh : ∀ i,(d i:ℝ)≤256*s)
        (logn denError : ℝ) (hn : 0≤logn) (power : Fin M → ℝ)
        (hpower : ∑ j,power j≤0) :
        (Finset.univ.sum (fun j : Fin M => power j*logn+
          StageEntropy.labelCost s hs len m cmp err d j.val+
          (StageEntropy.looseCost s len err+denError))) ≤
            -(1/1200:ℝ)*totalLength len m + 256*uncovered s hs len m cmp err+
              residual (E := E) s len m err M Q denError := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.StageEntropy.labelCost, OAI.TorsionFreeZeroDivisors.StageEntropy.looseCost, OAI.TorsionFreeZeroDivisors.StageMass.totalLength, OAI.TorsionFreeZeroDivisors.StageMass.uncovered, OAI.TorsionFreeZeroDivisors.StageMass.residual

18. theorem OAI.TorsionFreeZeroDivisors.StageMass.decay line 238

    Source documentation

    Concrete finite selection input: only an actual uncovered-length bound and the independently controlled remainder are needed.

    theorem decay (M Q : ℕ) (hm : ∀ c,m c≤M) (hQ : Fintype.card C≤Q)
        (ν : E → ℤ) (hsmall : 2*(err:ℝ)<s-1)
        (herr : ∀ e,2*|(cmp.offset e:ℝ)-(ν e:ℝ)*s|+4≤err)
        (d : Underlying s len → ℤ) (hlow : ∀ i,(1/600:ℝ)*s/2≤d i)
        (hhigh : ∀ i,(d i:ℝ)≤256*s)
        (logn denError : ℝ) (hn : 0≤logn) (power : Fin M → ℝ)
        (hpower : ∑ j,power j≤0)
        (hb : (uncovered s hs len m cmp err:ℝ) ≤ StageFusion.epsilon (1/600) 256*totalLength len m)
        (he : residual (E := E) s len m err M Q denError ≤ totalLength len m/4800) :
    …

    Mentions: OAI.TorsionFreeZeroDivisors.StageMass.uncovered, OAI.TorsionFreeZeroDivisors.StageFusion.epsilon, OAI.TorsionFreeZeroDivisors.StageMass.totalLength, OAI.TorsionFreeZeroDivisors.StageMass.residual

19. def OAI.TorsionFreeZeroDivisors.BinProfiles.values line 262
20. def OAI.TorsionFreeZeroDivisors.BinProfiles.profiles line 263
21. theorem OAI.TorsionFreeZeroDivisors.BinProfiles.mem_values line 266
22. theorem OAI.TorsionFreeZeroDivisors.BinProfiles.card_values line 273
23. theorem OAI.TorsionFreeZeroDivisors.BinProfiles.card_profiles line 282
24. theorem OAI.TorsionFreeZeroDivisors.BinProfiles.cardinal_bound line 291

    Source documentation

    The number of all integer bin assignments is exponentially bounded by the actual full-block mass. There is no independence assumption between bins.

    theorem cardinal_bound (s : ℝ) (hs : 0<s) (len : C → ℕ) :
        ((profiles s len).card:ℝ) ≤ Real.exp
          (((∑ c,(len c:ℝ))/s)*Real.log (256*s+1)) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.BinProfiles.profiles

25. def OAI.TorsionFreeZeroDivisors.GridAsymptotics.exponent line 305
26. def OAI.TorsionFreeZeroDivisors.GridAsymptotics.N line 306
27. def OAI.TorsionFreeZeroDivisors.GridAsymptotics.R line 307
28. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.exponent_pos line 309
29. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.N_pos line 311
30. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.R_pos line 315
31. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.R_le_N line 321
32. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.denominator_le_sqrt line 327
33. def OAI.TorsionFreeZeroDivisors.GridAsymptotics.scale line 343
34. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.scale_bounds line 345
35. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.N_tendsto line 369
36. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.R_tendsto line 373
37. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.alignment_error_tendsto line 377
38. def OAI.TorsionFreeZeroDivisors.GridAsymptotics.Compatible line 392

    Source documentation

    Exactly the source compatibility test, before choosing the least u.

    def Compatible (d : ℕ) (L : ℝ) (offset : Fin d → ℤ) (u : ℕ) : Prop :=
    …

39. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.compatible_exists line 396
40. def OAI.TorsionFreeZeroDivisors.GridAsymptotics.chosenU line 401
41. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.chosen_spec line 404
42. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.chosen_min line 410
43. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.chosen_bound line 416
44. def OAI.TorsionFreeZeroDivisors.GridAsymptotics.chosenScale line 421
45. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.chosen_alignment line 424
46. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.scale_tendsto line 440

    Source documentation

    Uniformly over arbitrary schedules of all prescribed offsets.

    theorem scale_tendsto (d : ℕ) (offset : ℝ → Fin d → ℤ) :
        Tendsto (fun L => chosenScale d L (offset L)) atTop atTop := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.GridAsymptotics.chosenScale

47. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.relative_scale_tendsto line 446
48. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.grid_loss_tendsto line 458

    Source documentation

    Relative errors for lost cut blocks plus rounded block lengths.

    theorem grid_loss_tendsto (d : ℕ) (offset : ℝ → Fin d → ℤ) :
        Tendsto (fun L => chosenScale d L (offset L)/L + 1/chosenScale d L (offset L)) atTop (𝓝 0) := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.GridAsymptotics.chosenScale

49. def OAI.TorsionFreeZeroDivisors.GridAsymptotics.letterError line 465

    Source documentation

    A fixed integer loss shared by all comparison sides.

    def letterError (d : ℕ) (L : ℝ) (offset : Fin d → ℤ) : ℕ :=
    …

50. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.chosenScale_pos line 468
51. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.letterError_bounds line 473
52. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.uniform_alignment line 486
53. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.relative_error_tendsto line 503
54. theorem OAI.TorsionFreeZeroDivisors.GridAsymptotics.eventually_small_error line 521