`BookProof.EnergyBandDecomposition.lintegral_eq_tsum_band` [MeasurableSpace X] {μ : Measure X} (hε : 0 < ε) (hE : Measurable E) (f : X → ℂ) : ∫⁻ x, ‖f x‖ₑ ^ 2 ∂μ = ∑' k :...
ProvedBookProof.EnergyBandDecomposition.lintegral_eq_tsum_bandtheoremstimepiece
Prove the following Lean 4 theorem from ChapterEnergyBandDecomposition.
BookProof.EnergyBandDecomposition.lintegral_eq_tsum_band [MeasurableSpace X] {μ : Measure X} (hε : 0 < ε) (hE : Measurable E) (f : X → ℂ) : ∫⁻ x, ‖f x‖ₑ ^ 2 ∂μ = ∑' k : ℤ, ∫⁻ x in band E ε k, ‖f x‖ₑ ^ 2 ∂μ
Formalization note: Lean 4 identifier BookProof.EnergyBandDecomposition.lintegral_eq_tsum_band.
Preamble
-- Generated from ChapterEnergyBandDecomposition.lean — theorem BookProof.EnergyBandDecomposition.lintegral_eq_tsum_band
import Mathlib
import Definitions.Def_ChapterEnergyBandDecomposition
open BookProof.EnergyBandDecomposition
open MeasureTheory
variable {X : Type*} {E : X → ℝ} {ε : ℝ} {k : ℤ} {x : X}Formal statement
theorem BookProof.EnergyBandDecomposition.lintegral_eq_tsum_band [MeasurableSpace X] {μ : Measure X} (hε : 0 < ε)
(hE : Measurable E)
(f : X → ℂ) :
∫⁻ x, ‖f x‖ₑ ^ 2 ∂μ = ∑' k : ℤ, ∫⁻ x in band E ε k, ‖f x‖ₑ ^ 2 ∂μ := by sorry