Commit 2026-09-30 08:09 f58d2cce

View on Github →

feat(Analysis/Subadditive): multiplicative Fekete's lemma (#42605) This PR proves Fekete's lemma for nonnegative submultiplicative sequences (the nth roots of a submultiplicative sequence converge). This will be applied to the sequence ‖a ^ k‖ ^ (k : ℝ)⁻¹ in a normed ring.

Estimated changes

Modified Mathlib/Analysis/Subadditive.lean

added theorem Subadditive.submultiplicative_exp

deleted def Subadditive

added theorem Submultiplicative.apply_mul_add_le

added theorem Submultiplicative.eventually_rpow_lt_of_rpow_lt

added theorem Submultiplicative.lim_le_rpow

added theorem Submultiplicative.tendsto_lim

added def Submultiplicative