Fermat's Last Theorem in Lean 4

Namespace `AnalyticOnNhd` 4 theorems

Integrability of log‖F‖ on a disc AnalyticOnNhd.integrableOn_log_norm_ball 2 below · cited by 3 · depth 23
Solid sub-mean-value inequality for log‖F‖-kg on a disc AnalyticOnNhd.log_norm_sub_mul_le_setAverage_ball 6 below · cited by 2 · depth 23
Sub-mean-value inequality for log‖F‖ on circles AnalyticOnNhd.log_norm_le_circleAverage_log_norm 0 below · cited by 2 · depth 24
Weighted sub-mean-value inequality for log‖F‖ AnalyticOnNhd.log_norm_sub_mul_le_circleAverage 1 below · cited by 1 · depth 24

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.