Commit 2021-03-17 19:18 41191815

View on Github →

feat(measure_theory/l2_space): L2 is an inner product space (#6596) If E is an inner product space, then so is Lp E 2 µ, with inner product being the integral of the inner products between function values.

Estimated changes

Modified docs/undergrad.yaml

Modified src/algebra/group_power/basic.lean

added theorem sub_pow_two

added theorem two_mul_le_add_pow_two

Modified src/algebra/ordered_field.lean

added theorem half_le_self

Modified src/analysis/normed_space/inner_product.lean

added theorem ae_measurable.inner

Modified src/measure_theory/bochner_integration.lean

Modified src/measure_theory/l1_space.lean

added theorem measure_theory.lipschitz_with.integrable_comp_iff_of_antilipschitz

Created src/measure_theory/l2_space.lean

added theorem measure_theory.L2.inner_def

added theorem measure_theory.L2.integrable_inner

added theorem measure_theory.L2.integral_inner_eq_sq_snorm

added theorem measure_theory.L2.mem_L1_inner

added theorem measure_theory.L2.snorm_inner_lt_top

added theorem measure_theory.L2.snorm_rpow_two_norm_lt_top

Modified src/measure_theory/lp_space.lean

added theorem lipschitz_with.mem_ℒp_comp_iff_of_antilipschitz

Modified src/measure_theory/prod.lean

Modified src/measure_theory/set_integral.lean

added theorem continuous_linear_map.integral_comp_comm'

added theorem integral_conj

added theorem integral_of_real

added theorem linear_isometry.integral_comp_comm

Modified src/topology/metric_space/antilipschitz.lean

added theorem antilipschitz_with.closed_embedding

Modified src/topology/metric_space/isometry.lean

added theorem isometry.closed_embedding