ProofAtlas

Lean evidence record

Fourier L¹/L² Compatibility Bridge: Lean evidence

This technical record binds the exact theorem statement to its commit-pinned Lean source, checker results, assumptions, and publication-review status.

Read theorem page
Lean buildpassed
Unfinished proof stepsNone
Publication reviewsAccepted

Exact recorded Lean statement

The declaration this evidence supports

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)) : ℝ → ℂ)

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.

Technical evidence record

Source identity, checker results, and assumptions

Main Lean declaration
fourier_ae_eq_l2_fourier_of_memLp_one_two
Source commit
f9c21e39b32d

Mechanical evidence

Lean verification

These fields support the exact Lean declaration, not a broader informal claim.

Artifact ID
artifact.known-fourier-l1-l2-compatibility.bridge.v002
Accepted-result title
Accepted Result: Fourier L1/L2 Compatibility Bridge: A.E.
Accepted-result status
Accepted formalization of a known theorem
Accepted-result boundary
This target records the narrow ℝ -> ℂ, volume-measure L1/L2 Fourier compatibility bridge: the function-level Fourier transform agrees almost everywhere with the L2 Fourier representative for functions in both L1 and L2. Non-claim: This is not a general finite-dimensional or vector-valued Fourier compatibility theorem. Non-claim: This does not discharge any PhysAtlas QHO theorem by itself. Non-claim: This accepted-result record does not establish novelty and does not by itself authorize public export or deployment.
Declarations covered by recorded evidence
AtlasKnownTheorems.FourierL1L2Compatibility.fourier_ae_eq_l2_fourier_of_memLp_one_two
AtlasKnownTheorems.FourierL1L2Compatibility.function_fourier_eLpNorm_eq_of_memLp_one_two
AtlasKnownTheorems.FourierL1L2Compatibility.function_fourier_l2_tempered_bridge
Lean build
passed
Recorded build time
16.4 s one machine-dependent evidence run, not a benchmark
Evidence collected
· clean-source provenance recorded
Unfinished proof check
passed
Lean toolchain
leanprover/lean4:v4.29.1
Recorded source commit
f9c21e39b32d19afeccc365edac6f2f4a3b2caa9
Source SHA-256
sha256:5c5fa4a621e587b9fada2949a0730a574ec38377b1a529c586fdc8cdb5406e3d
Statement alignment
accepted

Lean foundations

Standard foundations used by the proof

Lean reports the logical foundations below through Mathlib. They are standard proof-system foundations, not conjectural mathematical assumptions about this theorem. The recorded closure stays within the approved classical_mathlib_standard profile, with no unexpected axiom or unfinished-proof placeholder.

  • Classical.choice
  • Quot.sound
  • propext

Files and machine-readable evidence

Reproduce or inspect the recorded check

Use the complete first-party source bundle for reconstruction, or inspect the exact main file and checker evidence separately. Mathlib and other third-party dependencies are identified but not rebundled.

Complete checked Lean source · 1 Lean file · 1 evidence record · Download ZIPBrowse counted source onlineDownload main Lean fileDownload checker evidence (JSON)Download Apache-2.0 license

Review results

Publication reviews accepted

All four required publication-review gates are accepted for the reviewed presentation of this exact theorem. The review results are separate from the Lean build and do not broaden the formal statement.

Read the publication-review details