Fermat's Last Theorem in Lean 4

Namespace `MellinParseval` 3 theorems

Integrability of the Mellin profile of a strip-holomorphic family MellinParseval.integrableOn_Ioi_rpow_mul_lineIntegral_of_differentiableOn_of_norm_le 0 below · cited by 1 · depth 36
Mellin inversion on the unitary line MellinParseval.setIntegral_Ioi_inv_mul_cpow_neg_mul_lineIntegral_eq_two_pi_mul 0 below · cited by 1 · depth 36
Mellin–Plancherel identity along a vertical line MellinParseval.integrableOn_and_setIntegral_Ioi_norm_sq_lineIntegral_eq_two_pi_mul_integral_of_memLp_two 0 below · cited by 1 · depth 40

Documents the Lean sources in this repository (Lean v4.33.1, Mathlib v4.33.0). Statements are quoted textually from the .lean files; dependency edges are the import Theorems.Thm_… lines of the proof modules. About these pages.