Fermat's Last Theorem in Lean 4

Namespace `LocalParametrix` 6 theorems

Local fundamental solution with continuous kernels near x₀ LocalParametrix.exists_continuous_hasCompactSupport_apply_eq_integral_iterate_sum_iteratedFDeriv_add_integral_of_span_eq_top 4 below · cited by 1 · depth 32
Averaging a local parametrix pair over a compact linear group LocalParametrix.exists_continuous_hasCompactSupport_invariant_apply_eq_integral_add_integral_of_compactSpace 0 below · cited by 1 · depth 32
Continuous fundamental pair for an elliptic power of linear vector fields LocalParametrix.exists_continuous_contDiffOn_apply_eq_integral_iterate_sum_iteratedFDeriv_add_integral_of_span_eq_top 2 below · cited by 1 · depth 33
Localising a fundamental kernel smooth off its pole LocalParametrix.exists_hasCompactSupport_apply_eq_integral_add_integral_of_contDiffOn_compl_singleton 0 below · cited by 1 · depth 33
Fourier transform of a decaying symbol: continuity and smoothness off 0 LocalParametrix.continuous_fourier_and_contDiffOn_compl_zero_of_norm_iteratedFDeriv_le 0 below · cited by 1 · depth 34
Parametrix symbol of order -2m for an elliptic frequency-side operator LocalParametrix.exists_symbol_norm_iteratedFDeriv_le_integrable_iterate_sub_one_of_span_eq_top 0 below · cited by 1 · depth 34

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.