`BookProof.ChapterLinftyMaximalAbelian.symbol_ae_eq` (T : Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ) : (T (oneLp μ) : α → ℂ) =ᵐ[μ] symbol T
ProvedBookProof.ChapterLinftyMaximalAbelian.symbol_ae_eqtheoremstimepiece
Prove the following Lean 4 theorem from ChapterLinftyMaximalAbelian.
BookProof.ChapterLinftyMaximalAbelian.symbol_ae_eq (T : Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ) : (T (oneLp μ) : α → ℂ) =ᵐ[μ] symbol T
Formalization note: Lean 4 identifier BookProof.ChapterLinftyMaximalAbelian.symbol_ae_eq.
Preamble
-- Generated from ChapterLinftyMaximalAbelian.lean — theorem BookProof.ChapterLinftyMaximalAbelian.symbol_ae_eq
import Definitions.Def_ChapterLinftyMultiplication
import Mathlib
import Definitions.Def_ChapterLinftyMaximalAbelian
open BookProof.ChapterLinftyMaximalAbelian
noncomputable section
open MeasureTheory ENNReal Complex
open BookProof.ChapterLinftyMultiplication
variable {α : Type*} [MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ]Formal statement
theorem BookProof.ChapterLinftyMaximalAbelian.symbol_ae_eq (T : Lp ℂ 2 μ →L[ℂ] Lp ℂ 2 μ) :
(T (oneLp μ) : α → ℂ) =ᵐ[μ] symbol T := by sorry