Commit 2023-06-07 13:56 2d45c79c

View on Github →

feat: port MeasureTheory.Function.L2Space (#4737)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/GroupPower/Order.lean

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

Created Mathlib/MeasureTheory/Function/L2Space.lean

added theorem MeasureTheory.BoundedContinuousFunction.inner_toLp

added theorem MeasureTheory.ContinuousMap.inner_toLp

added theorem MeasureTheory.Integrable.const_inner

added theorem MeasureTheory.Integrable.inner_const

added theorem MeasureTheory.L2.inner_def

added theorem MeasureTheory.L2.inner_indicatorConstLp_eq_inner_set_integral

added theorem MeasureTheory.L2.inner_indicatorConstLp_eq_set_integral_inner

added theorem MeasureTheory.L2.inner_indicatorConstLp_one

added theorem MeasureTheory.L2.integrable_inner

added theorem MeasureTheory.L2.integral_inner_eq_sq_snorm

added theorem MeasureTheory.L2.mem_L1_inner

added theorem MeasureTheory.L2.snorm_inner_lt_top

added theorem MeasureTheory.L2.snorm_rpow_two_norm_lt_top

added theorem MeasureTheory.Memℒp.const_inner

added theorem MeasureTheory.Memℒp.inner_const

added theorem MeasureTheory.Memℒp.integrable_sq

added theorem MeasureTheory.memℒp_two_iff_integrable_sq

added theorem MeasureTheory.memℒp_two_iff_integrable_sq_norm

added theorem integral_eq_zero_of_forall_integral_inner_eq_zero

added theorem integral_inner