OAI/Analysis/Littlewood/FiniteFlatness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite positive real power-moment flatness for one all-length real-sign family.

  1. theorem OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.main line 14

    Source documentation

    One all-length real-sign family, simultaneously for every finite positive real exponent.

    Distinct definitions of this name: ComparatorChallenges/LittlewoodFiniteFlatness.lean:34 (same statement text; different proof or body). Qualify references as OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.main@path.

    theorem main : MainStatement := by
…

    Mentions: OAI.AsymptoticallyMinimalLittlewoodFiniteFlatness.MainStatement