Formal evidence
Independent review accepted the recorded build, exact declarations, unfinished-step scan, and axiom evidence.
Analysis · formal theorem
Fourier L¹/L² Compatibility Bridge
The function-level Fourier transform agrees almost everywhere with its L² representative for ℝ → ℂ functions in both L¹ and L².
Lean proofpassed
Unfinished proof stepsNone
Formal resultAccepted
Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.
The theorem at a glance
Fourier L¹/L² compatibility at a glance
Accessible transcript
f ∈ L¹ ∩ L² ⇒ ℱfunction(f) =ᵐ ℱL²([f])
The checked proof embeds the L² representative as a tempered distribution, matches both transforms against smooth compactly supported tests, and uses local integrability to conclude almost-everywhere equality. It identifies representatives only up to a null set, not pointwise.
Read the complete poster transcript
FOURIER ANALYSIS · REPRESENTATIVE COMPATIBILITY
ONE TRANSFORM, TWO CONSTRUCTIONS
FOR f : ℝ → ℂ WITH f ∈ L¹ ∩ L²
ℱfunction(f) =ᵐ ℱL²([f])
Equality holds almost everywhere.
f
FUNCTION-LEVEL ROUTE
L¹ makes the integral Fourier transform available.
ℱfunction(f)(ξ) = ∫ℝ f(x)e⁻²πixξ dx
e⁻²πixξ
L² ROUTE
L² supplies the unitary Fourier representative.
ℱL²([f]) ∈ L²(ℝ)
(unitary Fourier transform)
L²
Equal almost everywhere.
Differences can occur only on a set of measure zero.
THE BRIDGE
The two transforms give the same value against every smooth compactly supported test.
HOW THE PROOF MOVES
1 · EMBED THE L² TRANSFORM
View the L² representative as a tempered distribution.
2 · MATCH TEST INTEGRALS
φ
Schwartz duality identifies both actions.
3 · USE LOCAL INTEGRABILITY
Equal compactly supported tests force a.e. equality.
4 · IDENTIFY THE REPRESENTATIVES
ℱfunction(f) =ᵐ ℱL²([f])
EXACT SCOPE
Almost-everywhere equality for f ∈ L¹ ∩ L². Not pointwise equality, not a claim for arbitrary L² functions, and not a discrete Fourier transform.
Theorem schematic
Two Fourier constructions, one a.e. transform
f ∈ L¹ ∩ L² ⇒ ℱfunction(f) =ᵐ ℱL²([f])
When f belongs to both L¹ and L², its oscillatory-integral Fourier transform and its unitary L² Fourier representative determine the same measurable function almost everywhere. The theorem does not assert pointwise equality or cover arbitrary L² inputs.
Exact formal proposition
Hypotheses and conclusion
theorem fourier_ae_eq_l2_fourier_of_memLp_one_two
{f : ℝ → ℂ}
(hf_one : MeasureTheory.MemLp f 1 MeasureTheory.volume)
(hf_two : MeasureTheory.MemLp f 2 MeasureTheory.volume) :
FourierTransform.fourier f =ᵐ[MeasureTheory.volume]
((FourierTransform.fourier
(hf_two.toLp f : MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ℝ → ℂ)Result boundary
What this page does—and does not—establish
The narrow ℝ → ℂ, volume-measure L¹/L² Fourier compatibility bridge: the function-level Fourier transform agrees almost everywhere with the L² Fourier representative for functions in both L¹ and L².
- This is not a general finite-dimensional or vector-valued Fourier compatibility theorem.
About these visual explanations
These AI-generated visuals explain the theorem and proof route; they are not proof evidence. Their publication review was completed separately from review of the formal result. The exact Lean proposition and checked source remain authoritative.
Continue the mathematics
Start from the complete checked source
The pinned theorem and its complete local import closure let internal and external agents inspect the proof, compare an alternate route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks every proposed extension against its exact formal statement.
The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and an agent continuation file. Mathlib and other third-party dependencies are not bundled.
Formal-result publication and review details
Independent publication review
The formal theorem's publication gates are accepted
Lean checks the proof. Independent AI review separately accepted evidence completeness, statement alignment, result boundary, and the retained theorem wording. Those gates apply to the formal result; generated media is reviewed and promoted separately. Neither review replaces Lean's proof check or broadens the theorem.
Statement alignment
The formal declaration was accepted against the named theorem and its exact variant.
Result boundary
The accepted boundary keeps nearby stronger or commonly confused claims out of scope.
Public wording
Independent review accepted the retained theorem explanation and source presentation. Generated media follows a separate review and promotion gate.
Canonical source
The first-party source link is pinned to the checked package commit and exact Lean file.
Accepted result
A validated accepted-result record binds the four reviews to the checked formalization.