5.1. Mathlib candidates: Lp and measure transport🔗

General measure-transport lemmas and bounded-operator infrastructure on Bochner Lp spaces. These declarations form a dependency boundary used by the Fourier and representation-theoretic pages.

Lp spaces

Theorem5.1.1

uses 0used by 1✓L∃∀N

Density of the integrable elements in Lp. For an exponent 1\le p<\infty, the classes in L^p(\mu) with an integrable representative — that is, L^1\cap L^p(\mu) — form a dense subset of L^p(\mu). Mathlib provides the density of Lp simple functions (MeasureTheory.Lp.simpleFunc.dense) and the integrability of Lp simple functions (MeasureTheory.SimpleFunc.memLp_iff_integrable) separately, but not this combination, which is the standard entry point for extending an operator defined by an absolutely convergent integral on L^1\cap L^p to all of L^p.

Lean code for Theorem5.1.1●1 theorem

theoremdefined in LeanRidgelet/ToMathlib/LpIntegrableDense.lean

complete

theorem MeasureTheory.Lp.dense_setOf_integrable.{u_1, u_2} {α : Type u_1}
  {E : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [NormedAddCommGroup E] {p : ENNReal} [Fact (1 ≤ p)]
  (hp_ne_top : p ≠ ⊤) : Dense {f | MeasureTheory.Integrable (↑↑f) μ}

theorem MeasureTheory.Lp.dense_setOf_integrable.{u_1,
    u_2}
  {α : Type u_1} {E : Type u_2}
  [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  [NormedAddCommGroup E] {p : ENNReal}
  [Fact (1 ≤ p)] (hp_ne_top : p ≠ ⊤) :
  Dense
    {f | MeasureTheory.Integrable (↑↑f) μ}

For `p ≠ ∞`, the classes in `Lp E p μ` with an integrable representative are dense; this is
the density of `L¹ ∩ L^p` in `L^p`.

Theorem5.1.2

uses 0used by 1✓L∃∀N

Unimodular multiplication on Lp. An almost-everywhere strongly measurable complex function u with |u|=1 acts on every normed L^p(\mu) by pointwise multiplication. The action is bundled as a linear isometric equivalence, has u f as its almost-everywhere representative, and is onto because multiplication by \overline u gives a preimage. The proof uses Mathlib's MemLp.congr_norm and does not require a separate integrability estimate.

Lean code for Theorem5.1.2●6 declarations

theoremdefined in LeanRidgelet/ToMathlib/LpUnimodular.lean

complete

theorem MeasureTheory.MemLp.unimodular_mul.{u_1} {X : Type u_1}
  [MeasurableSpace X] {p : ENNReal} {μ : MeasureTheory.Measure X}
  (u : X → ℂ) (hu : MeasureTheory.AEStronglyMeasurable u μ)
  (hunimodular : ∀ᵐ (x : X) ∂μ, ‖u x‖ = 1)
  (f : ↥(MeasureTheory.Lp ℂ p μ)) :
  MeasureTheory.MemLp (fun x ↦ u x * ↑↑f x) p μ

theorem MeasureTheory.MemLp.unimodular_mul.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  (u : X → ℂ)
  (hu :
    MeasureTheory.AEStronglyMeasurable u
      μ)
  (hunimodular : ∀ᵐ (x : X) ∂μ, ‖u x‖ = 1)
  (f : ↥(MeasureTheory.Lp ℂ p μ)) :
  MeasureTheory.MemLp
    (fun x ↦ u x * ↑↑f x) p μ

Pointwise multiplication by an a.e. unimodular measurable function preserves `MemLp`.

defdefined in LeanRidgelet/ToMathlib/LpUnimodular.lean

complete

def MeasureTheory.unimodularMultiplierLinearIsometry.{u_1} {X : Type u_1}
  [MeasurableSpace X] {p : ENNReal} {μ : MeasureTheory.Measure X}
  (u : X → ℂ) (hu : MeasureTheory.AEStronglyMeasurable u μ)
  (hunimodular : ∀ᵐ (x : X) ∂μ, ‖u x‖ = 1) [Fact (1 ≤ p)] :
  ↥(MeasureTheory.Lp ℂ p μ) →ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ p μ)

def MeasureTheory.unimodularMultiplierLinearIsometry.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  (u : X → ℂ)
  (hu :
    MeasureTheory.AEStronglyMeasurable u
      μ)
  (hunimodular : ∀ᵐ (x : X) ∂μ, ‖u x‖ = 1)
  [Fact (1 ≤ p)] :
  ↥(MeasureTheory.Lp ℂ p μ) →ₗᵢ[ℂ]
    ↥(MeasureTheory.Lp ℂ p μ)

Implementation after :=

:= (MemLp.unimodular_mul u hu hunimodular f).toLp _
  map_add' f g := by
    let hsum := MemLp.unimodular_mul u hu hunimodular (f + g)
    let hf := MemLp.unimodular_mul u hu hunimodular f
    let hg := MemLp.unimodular_mul u hu hunimodular g
    change hsum.toLp _ = hf.toLp _ + hg.toLp _
    rw [← MemLp.toLp_add]
    apply MemLp.toLp_congr
    filter_upwards [Lp.coeFn_add f g] with x hx
    rw [hx]
    simpa only [Pi.add_apply] using mul_add (u x) (f x) (g x)
  map_smul' c f := by
    let hcf := MemLp.unimodular_mul u hu hunimodular (c • f)
    let hf := MemLp.unimodular_mul u hu hunimodular f
    change hcf.toLp _ = c • hf.toLp _
    rw [← MemLp.toLp_const_smul]
    apply MemLp.toLp_congr
    filter_upwards [Lp.coeFn_smul c f] with x hx
    rw [hx]
    simp only [Pi.smul_apply, smul_eq_mul]
    ring
  norm_map' f := by
    let hf := MemLp.unimodular_mul u hu hunimodular f
    change ‖hf.toLp _‖ = ‖f‖
    calc
      ‖hf.toLp _‖ = ENNReal.toReal (eLpNorm (fun x ↦ u x * f x) p μ) :=
        Lp.norm_toLp _ hf
      _ = ENNReal.toReal (eLpNorm (fun x ↦ f x) p μ) := by
        apply congrArg ENNReal.toReal
        apply eLpNorm_congr_norm_ae
        filter_upwards [hunimodular] with x hx
        simp only [norm_mul, hx, one_mul]
      _ = ‖f‖ := (Lp.norm_def f).symm

Pointwise multiplication by an a.e. unimodular measurable function, as an `Lp` linear
isometry.

theoremdefined in LeanRidgelet/ToMathlib/LpUnimodular.lean

complete

theorem MeasureTheory.unimodularMultiplierLinearIsometry_apply_ae.{u_1}
  {X : Type u_1} [MeasurableSpace X] {p : ENNReal}
  {μ : MeasureTheory.Measure X} (u : X → ℂ)
  (hu : MeasureTheory.AEStronglyMeasurable u μ)
  (hunimodular : ∀ᵐ (x : X) ∂μ, ‖u x‖ = 1) [Fact (1 ≤ p)]
  (f : ↥(MeasureTheory.Lp ℂ p μ)) :
  ↑↑((MeasureTheory.unimodularMultiplierLinearIsometry u hu hunimodular)
          f) =ᵐ[μ]
    fun x ↦ u x * ↑↑f x

theorem MeasureTheory.unimodularMultiplierLinearIsometry_apply_ae.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  (u : X → ℂ)
  (hu :
    MeasureTheory.AEStronglyMeasurable u
      μ)
  (hunimodular : ∀ᵐ (x : X) ∂μ, ‖u x‖ = 1)
  [Fact (1 ≤ p)]
  (f : ↥(MeasureTheory.Lp ℂ p μ)) :
  ↑↑((MeasureTheory.unimodularMultiplierLinearIsometry
            u hu hunimodular)
          f) =ᵐ[μ]
    fun x ↦ u x * ↑↑f x

The `Lp` isometry given by an a.e. unimodular multiplier has the expected pointwise
representative.

theoremdefined in LeanRidgelet/ToMathlib/LpUnimodular.lean

complete

theorem MeasureTheory.unimodularMultiplierLinearIsometry_surjective.{u_1}
  {X : Type u_1} [MeasurableSpace X] {p : ENNReal}
  {μ : MeasureTheory.Measure X} (u : X → ℂ)
  (hu : MeasureTheory.AEStronglyMeasurable u μ)
  (hunimodular : ∀ᵐ (x : X) ∂μ, ‖u x‖ = 1) [Fact (1 ≤ p)] :
  Function.Surjective
    ⇑(MeasureTheory.unimodularMultiplierLinearIsometry u hu hunimodular)

theorem MeasureTheory.unimodularMultiplierLinearIsometry_surjective.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  (u : X → ℂ)
  (hu :
    MeasureTheory.AEStronglyMeasurable u
      μ)
  (hunimodular : ∀ᵐ (x : X) ∂μ, ‖u x‖ = 1)
  [Fact (1 ≤ p)] :
  Function.Surjective
    ⇑(MeasureTheory.unimodularMultiplierLinearIsometry
        u hu hunimodular)

Pointwise multiplication by an a.e. unimodular measurable function is onto: conjugating the
multiplier gives an explicit preimage.

defdefined in LeanRidgelet/ToMathlib/LpUnimodular.lean

complete

def MeasureTheory.unimodularMultiplierLinearIsometryEquiv.{u_1}
  {X : Type u_1} [MeasurableSpace X] {p : ENNReal}
  {μ : MeasureTheory.Measure X} (u : X → ℂ)
  (hu : MeasureTheory.AEStronglyMeasurable u μ)
  (hunimodular : ∀ᵐ (x : X) ∂μ, ‖u x‖ = 1) [Fact (1 ≤ p)] :
  ↥(MeasureTheory.Lp ℂ p μ) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ p μ)

def MeasureTheory.unimodularMultiplierLinearIsometryEquiv.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  (u : X → ℂ)
  (hu :
    MeasureTheory.AEStronglyMeasurable u
      μ)
  (hunimodular : ∀ᵐ (x : X) ∂μ, ‖u x‖ = 1)
  [Fact (1 ≤ p)] :
  ↥(MeasureTheory.Lp ℂ p μ) ≃ₗᵢ[ℂ]
    ↥(MeasureTheory.Lp ℂ p μ)

Implementation after :=

:=
  LinearIsometryEquiv.ofSurjective (unimodularMultiplierLinearIsometry u hu hunimodular)
    (unimodularMultiplierLinearIsometry_surjective u hu hunimodular)

Pointwise multiplication by an a.e. unimodular measurable function, as a linear isometric
equivalence of `Lp`.

theoremdefined in LeanRidgelet/ToMathlib/LpUnimodular.lean

complete

theorem MeasureTheory.unimodularMultiplierLinearIsometryEquiv_apply_ae.{u_1}
  {X : Type u_1} [MeasurableSpace X] {p : ENNReal}
  {μ : MeasureTheory.Measure X} (u : X → ℂ)
  (hu : MeasureTheory.AEStronglyMeasurable u μ)
  (hunimodular : ∀ᵐ (x : X) ∂μ, ‖u x‖ = 1) [Fact (1 ≤ p)]
  (f : ↥(MeasureTheory.Lp ℂ p μ)) :
  ↑↑((MeasureTheory.unimodularMultiplierLinearIsometryEquiv u hu
            hunimodular)
          f) =ᵐ[μ]
    fun x ↦ u x * ↑↑f x

theorem MeasureTheory.unimodularMultiplierLinearIsometryEquiv_apply_ae.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  (u : X → ℂ)
  (hu :
    MeasureTheory.AEStronglyMeasurable u
      μ)
  (hunimodular : ∀ᵐ (x : X) ∂μ, ‖u x‖ = 1)
  [Fact (1 ≤ p)]
  (f : ↥(MeasureTheory.Lp ℂ p μ)) :
  ↑↑((MeasureTheory.unimodularMultiplierLinearIsometryEquiv
            u hu hunimodular)
          f) =ᵐ[μ]
    fun x ↦ u x * ↑↑f x

The bundled unimodular multiplier has the expected pointwise representative.

Quasi-invariant measure transport

Theorem5.1.3

uses 0used by 1✓L∃∀N

Bochner change of variables for a quasi-invariant measure. If pushforward by x\mapsto g^{-1}x has nonnegative density J_g with respect to \mu, then every Bochner integrand satisfies \int F\,d\mu=\int J_g(x)F(gx)\,d\mu. The proof packages the action as a measurable equivalence, applies integral_map_equiv, and rewrites the resulting withDensity integral. The companion identity J\cdot J^{-1/2}y=J^{1/2}y for nonzero J is the algebraic cancellation needed by unitary Radon--Nikodym multipliers.

Lean code for Theorem5.1.3●2 theorems

theoremdefined in LeanRidgelet/ToMathlib/QuasiInvariantIntegral.lean

complete

theorem MeasureTheory.integral_eq_integral_smul_comp_smul_of_map_eq_withDensity.{u_1,
    u_2, u_3}
  {G : Type u_1} {X : Type u_2} {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E]
  (μ : MeasureTheory.Measure X) (jacobian : G → X → NNReal)
  (h_measurable : ∀ (g : G), Measurable fun x ↦ g • x)
  (h_map :
    ∀ (g : G),
      MeasureTheory.Measure.map (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦ ↑(jacobian g x))
  (h_jacobian : ∀ (g : G), Measurable (jacobian g)) (g : G)
  (F : X → E) :
  ∫ (x : X), F x ∂μ = ∫ (x : X), jacobian g x • F (g • x) ∂μ

theorem MeasureTheory.integral_eq_integral_smul_comp_smul_of_map_eq_withDensity.{u_1,
    u_2, u_3}
  {G : Type u_1} {X : Type u_2}
  {E : Type u_3} [Group G] [MulAction G X]
  [MeasurableSpace X]
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  (μ : MeasureTheory.Measure X)
  (jacobian : G → X → NNReal)
  (h_measurable :
    ∀ (g : G), Measurable fun x ↦ g • x)
  (h_map :
    ∀ (g : G),
      MeasureTheory.Measure.map
          (fun x ↦ g⁻¹ • x) μ =
        μ.withDensity fun x ↦
          ↑(jacobian g x))
  (h_jacobian :
    ∀ (g : G), Measurable (jacobian g))
  (g : G) (F : X → E) :
  ∫ (x : X), F x ∂μ =
    ∫ (x : X), jacobian g x • F (g • x) ∂μ

A Bochner change-of-variables formula for a quasi-invariant measure. The hypothesis says
that pushforward by `x ↦ g⁻¹ • x` has density `jacobian g` with respect to `μ`; the conclusion
moves the action from the measure to the integrand and inserts that density as a real scalar.

theoremdefined in LeanRidgelet/ToMathlib/QuasiInvariantIntegral.lean

complete

theorem NNReal.smul_inv_sqrt_smul.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℂ E] (j : NNReal) (hj : j ≠ 0) (y : E) :
  j • (↑↑(NNReal.sqrt j))⁻¹ • y = ↑↑(NNReal.sqrt j) • y

theorem NNReal.smul_inv_sqrt_smul.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℂ E] (j : NNReal)
  (hj : j ≠ 0) (y : E) :
  j • (↑↑(NNReal.sqrt j))⁻¹ • y =
    ↑↑(NNReal.sqrt j) • y

Multiplication by a nonzero nonnegative real cancels one inverse square-root factor.

Theorem5.1.4

uses 0used by 1✓L∃∀N

Continuous preimages for constant-density maps. Suppose continuous maps r_i:X\to Y converge in the compact-open topology, their pushforward measures are c_i\mu, and the finite nonnegative constants c_i converge. Then the preimages of every finite-measure measurable set converge in symmetric-difference measure. The proof first treats open sets using inner regularity and compact-open convergence, then approximates a measurable set by an open set. This extends Mathlib's corresponding measure-preserving result to the determinant-scaled maps required by quasi-regular affine actions.

Lean code for Theorem5.1.4●3 theorems

theoremdefined in LeanRidgelet/ToMathlib/ContinuousConstDensityPreimage.lean

complete

theorem MeasureTheory.measure_preimage_eq_nnreal_smul.{u_2, u_3} {X : Type u_2}
  {Y : Type u_3} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X]
  [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y]
  {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y}
  {f : C(X, Y)} {c : NNReal}
  (hmap : MeasureTheory.Measure.map (⇑f) μ = ↑c • ν) {s : Set Y}
  (hs : MeasurableSet s) : μ (⇑f ⁻¹' s) = ↑c * ν s

theorem MeasureTheory.measure_preimage_eq_nnreal_smul.{u_2,
    u_3}
  {X : Type u_2} {Y : Type u_3}
  [TopologicalSpace X] [MeasurableSpace X]
  [BorelSpace X] [TopologicalSpace Y]
  [MeasurableSpace Y] [BorelSpace Y]
  {μ : MeasureTheory.Measure X}
  {ν : MeasureTheory.Measure Y}
  {f : C(X, Y)} {c : NNReal}
  (hmap :
    MeasureTheory.Measure.map (⇑f) μ =
      ↑c • ν)
  {s : Set Y} (hs : MeasurableSet s) :
  μ (⇑f ⁻¹' s) = ↑c * ν s

If the pushforward of `μ` is a finite scalar multiple of `ν`, preimages of measurable sets
have the correspondingly scaled measure.

theoremdefined in LeanRidgelet/ToMathlib/ContinuousConstDensityPreimage.lean

complete

theorem MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero_of_isOpen_of_map_eq_nnreal_smul.{u_1,
    u_2, u_3}
  {α : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X]
  [MeasurableSpace X] [BorelSpace X] [R1Space X] [TopologicalSpace Y]
  [MeasurableSpace Y] [BorelSpace Y] {μ : MeasureTheory.Measure X}
  {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop]
  {l : Filter α} {f : α → C(X, Y)} {g : C(X, Y)} {c : α → NNReal}
  {d : NNReal} {s : Set Y} (hfg : Filter.Tendsto f l (nhds g))
  (hc : Filter.Tendsto c l (nhds d))
  (hf :
    ∀ᶠ (a : α) in l, MeasureTheory.Measure.map (⇑(f a)) μ = ↑(c a) • ν)
  (hg : MeasureTheory.Measure.map (⇑g) μ = ↑d • ν) (hs : IsOpen s)
  (hνs : ν s ≠ ⊤) :
  Filter.Tendsto (fun a ↦ μ (symmDiff (⇑(f a) ⁻¹' s) (⇑g ⁻¹' s))) l
    (nhds 0)

theorem MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero_of_isOpen_of_map_eq_nnreal_smul.{u_1,
    u_2, u_3}
  {α : Type u_1} {X : Type u_2}
  {Y : Type u_3} [TopologicalSpace X]
  [MeasurableSpace X] [BorelSpace X]
  [R1Space X] [TopologicalSpace Y]
  [MeasurableSpace Y] [BorelSpace Y]
  {μ : MeasureTheory.Measure X}
  {ν : MeasureTheory.Measure Y}
  [μ.InnerRegularCompactLTTop]
  {l : Filter α} {f : α → C(X, Y)}
  {g : C(X, Y)} {c : α → NNReal}
  {d : NNReal} {s : Set Y}
  (hfg : Filter.Tendsto f l (nhds g))
  (hc : Filter.Tendsto c l (nhds d))
  (hf :
    ∀ᶠ (a : α) in l,
      MeasureTheory.Measure.map (⇑(f a))
          μ =
        ↑(c a) • ν)
  (hg :
    MeasureTheory.Measure.map (⇑g) μ =
      ↑d • ν)
  (hs : IsOpen s) (hνs : ν s ≠ ⊤) :
  Filter.Tendsto
    (fun a ↦
      μ
        (symmDiff (⇑(f a) ⁻¹' s)
          (⇑g ⁻¹' s)))
    l (nhds 0)

Preimages of a finite-measure open set vary continuously in symmetric-difference measure for
a convergent family of continuous maps whose pushforward measures have convergent constant
densities.

theoremdefined in LeanRidgelet/ToMathlib/ContinuousConstDensityPreimage.lean

complete

theorem MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero_of_map_eq_nnreal_smul.{u_1,
    u_2, u_3}
  {α : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X]
  [MeasurableSpace X] [BorelSpace X] [R1Space X] [TopologicalSpace Y]
  [MeasurableSpace Y] [BorelSpace Y] [R1Space Y]
  {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y}
  [μ.InnerRegularCompactLTTop] [ν.InnerRegularCompactLTTop]
  [MeasureTheory.IsLocallyFiniteMeasure ν] {l : Filter α}
  {f : α → C(X, Y)} {g : C(X, Y)} {c : α → NNReal} {d : NNReal}
  {s : Set Y} (hfg : Filter.Tendsto f l (nhds g))
  (hc : Filter.Tendsto c l (nhds d))
  (hf :
    ∀ᶠ (a : α) in l, MeasureTheory.Measure.map (⇑(f a)) μ = ↑(c a) • ν)
  (hg : MeasureTheory.Measure.map (⇑g) μ = ↑d • ν)
  (hs : MeasurableSet s) (hνs : ν s ≠ ⊤) :
  Filter.Tendsto (fun a ↦ μ (symmDiff (⇑(f a) ⁻¹' s) (⇑g ⁻¹' s))) l
    (nhds 0)

theorem MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero_of_map_eq_nnreal_smul.{u_1,
    u_2, u_3}
  {α : Type u_1} {X : Type u_2}
  {Y : Type u_3} [TopologicalSpace X]
  [MeasurableSpace X] [BorelSpace X]
  [R1Space X] [TopologicalSpace Y]
  [MeasurableSpace Y] [BorelSpace Y]
  [R1Space Y]
  {μ : MeasureTheory.Measure X}
  {ν : MeasureTheory.Measure Y}
  [μ.InnerRegularCompactLTTop]
  [ν.InnerRegularCompactLTTop]
  [MeasureTheory.IsLocallyFiniteMeasure ν]
  {l : Filter α} {f : α → C(X, Y)}
  {g : C(X, Y)} {c : α → NNReal}
  {d : NNReal} {s : Set Y}
  (hfg : Filter.Tendsto f l (nhds g))
  (hc : Filter.Tendsto c l (nhds d))
  (hf :
    ∀ᶠ (a : α) in l,
      MeasureTheory.Measure.map (⇑(f a))
          μ =
        ↑(c a) • ν)
  (hg :
    MeasureTheory.Measure.map (⇑g) μ =
      ↑d • ν)
  (hs : MeasurableSet s) (hνs : ν s ≠ ⊤) :
  Filter.Tendsto
    (fun a ↦
      μ
        (symmDiff (⇑(f a) ⁻¹' s)
          (⇑g ⁻¹' s)))
    l (nhds 0)

Let `f a : C(X, Y)` converge to `g` in the compact-open topology, and suppose that the
pushforward of `μ` under these maps is a finite constant multiple of `ν`, with multipliers
converging in `ℝ≥0`. Then preimages of every finite-measure measurable set converge in
symmetric-difference measure.

Theorem5.1.5

uses 0

Used by 5

Reverse dependency previews

Preview

Theorem 4.3.1

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Adjoints, block determinants, and affine Haar transport. In finite-dimensional inner-product spaces, the adjoint of a linear equivalence is bundled as an equivalence and its determinant is the conjugate determinant. A block lower-triangular LinearEquiv.skewProd has the product of its diagonal determinants. Finally, an affine equivalence x\mapsto Lx+t pushes an additive Haar measure forward by the scalar |\det L^{-1}|; the inverse map has the constant withDensity density \lVert\det L\rVert. The proof combines Mathlib's linear Haar change of variables with translation invariance.

Lean code for Theorem5.1.5●6 declarations

defdefined in LeanRidgelet/ToMathlib/AffineHaar.lean

complete

def LinearEquiv.adjoint.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F]
  [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F] (e : E ≃ₗ[𝕜] F) :
  F ≃ₗ[𝕜] E

def LinearEquiv.adjoint.{u_1, u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2}
  {F : Type u_3} [RCLike 𝕜]
  [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E]
  [NormedAddCommGroup F]
  [InnerProductSpace 𝕜 F]
  [FiniteDimensional 𝕜 F]
  (e : E ≃ₗ[𝕜] F) : F ≃ₗ[𝕜] E

Implementation after :=

:= (e : E →ₗ[𝕜] F).adjoint
  invFun := (e.symm : F →ₗ[𝕜] E).adjoint
  left_inv x := by
    have h := congrArg (fun f : F →ₗ[𝕜] F ↦ f x)
      (LinearMap.adjoint_comp (e : E →ₗ[𝕜] F) (e.symm : F →ₗ[𝕜] E))
    simpa using h.symm
  right_inv x := by
    have h := congrArg (fun f : E →ₗ[𝕜] E ↦ f x)
      (LinearMap.adjoint_comp (e.symm : F →ₗ[𝕜] E) (e : E →ₗ[𝕜] F))
    simpa using h.symm

The adjoint of a finite-dimensional linear equivalence, bundled as a linear equivalence in
the reverse direction.

theoremdefined in LeanRidgelet/ToMathlib/AffineHaar.lean

complete

theorem LinearMap.det_adjoint.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2}
  [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] (f : E →ₗ[𝕜] E) :
  LinearMap.det (LinearMap.adjoint f) = star (LinearMap.det f)

theorem LinearMap.det_adjoint.{u_1, u_2}
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E]
  (f : E →ₗ[𝕜] E) :
  LinearMap.det (LinearMap.adjoint f) =
    star (LinearMap.det f)

The determinant of the adjoint is the conjugate of the determinant.

theoremdefined in LeanRidgelet/ToMathlib/AffineHaar.lean

complete

theorem LinearEquiv.det_adjoint.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2}
  [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] (e : E ≃ₗ[𝕜] E) :
  LinearMap.det ↑e.adjoint = star (LinearMap.det ↑e)

theorem LinearEquiv.det_adjoint.{u_1, u_2}
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E]
  (e : E ≃ₗ[𝕜] E) :
  LinearMap.det ↑e.adjoint =
    star (LinearMap.det ↑e)

Determinant of the bundled adjoint equivalence.

theoremdefined in LeanRidgelet/ToMathlib/AffineHaar.lean

complete

theorem LinearEquiv.det_skewProd.{u_3, u_4, u_5} {R : Type u_3} {M : Type u_4}
  {N : Type u_5} [CommRing R] [AddCommGroup M] [Module R M]
  [Module.Free R M] [Module.Finite R M] [AddCommGroup N] [Module R N]
  [Module.Free R N] [Module.Finite R N] (e₁ : M ≃ₗ[R] M)
  (e₂ : N ≃ₗ[R] N) (f : M →ₗ[R] N) :
  LinearMap.det ↑(e₁.skewProd e₂ f) =
    LinearMap.det ↑e₁ * LinearMap.det ↑e₂

theorem LinearEquiv.det_skewProd.{u_3, u_4, u_5}
  {R : Type u_3} {M : Type u_4}
  {N : Type u_5} [CommRing R]
  [AddCommGroup M] [Module R M]
  [Module.Free R M] [Module.Finite R M]
  [AddCommGroup N] [Module R N]
  [Module.Free R N] [Module.Finite R N]
  (e₁ : M ≃ₗ[R] M) (e₂ : N ≃ₗ[R] N)
  (f : M →ₗ[R] N) :
  LinearMap.det ↑(e₁.skewProd e₂ f) =
    LinearMap.det ↑e₁ * LinearMap.det ↑e₂

The determinant of a block lower-triangular linear equivalence is the product of the
determinants of its diagonal blocks.

theoremdefined in LeanRidgelet/ToMathlib/AffineHaar.lean

complete

theorem MeasureTheory.Measure.map_affineEquiv_addHaar_eq_smul_addHaar.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E]
  (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (g : E ≃ᵃ[ℝ] E) :
  MeasureTheory.Measure.map (⇑g) μ =
    ENNReal.ofReal |LinearMap.det ↑g.linear.symm| • μ

theorem MeasureTheory.Measure.map_affineEquiv_addHaar_eq_smul_addHaar.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E]
  [BorelSpace E] [FiniteDimensional ℝ E]
  (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure] (g : E ≃ᵃ[ℝ] E) :
  MeasureTheory.Measure.map (⇑g) μ =
    ENNReal.ofReal
        |LinearMap.det ↑g.linear.symm| •
      μ

An affine equivalence rescales an additive Haar measure by the absolute determinant of its
inverse linear part.

theoremdefined in LeanRidgelet/ToMathlib/AffineHaar.lean

complete

theorem MeasureTheory.Measure.map_affineEquiv_symm_addHaar_eq_withDensity.{u_1}
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E]
  (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (g : E ≃ᵃ[ℝ] E) :
  MeasureTheory.Measure.map (⇑g.symm) μ =
    μ.withDensity fun x ↦ ↑‖LinearMap.det ↑g.linear‖₊

theorem MeasureTheory.Measure.map_affineEquiv_symm_addHaar_eq_withDensity.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E]
  [BorelSpace E] [FiniteDimensional ℝ E]
  (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure] (g : E ≃ᵃ[ℝ] E) :
  MeasureTheory.Measure.map (⇑g.symm) μ =
    μ.withDensity fun x ↦
      ↑‖LinearMap.det ↑g.linear‖₊

The inverse of an affine equivalence pushes Haar measure to the constant density given by the
absolute determinant of the forward linear part.

Hilbert-space duality and Lp operators

Theorem5.1.6

uses 0

Used by 4

Reverse dependency previews

Preview

Lemma 2.2.13

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Cauchy--Schwarz and an L² duality criterion. Two elementary tools that Mathlib states only in Lp-space form. First, Cauchy--Schwarz for Bochner integrals: for square-integrable scalar u, v, \Big\|\int u\,\overline v\Big\|\le\Big(\int\|u\|^2\Big)^{1/2}\Big(\int\|v\|^2\Big)^{1/2}, by Hölder's inequality for the norms. Second, an L² duality criterion: if h is measurable, the measurable sets s_n increase to the whole space, every truncation 1_{s_n}h is square-integrable, and \Big|\int h\,\overline{1_{s_n}h}\Big|\le M\,\|1_{s_n}h\|_2\quad\text{for all }n, then h itself is square-integrable with \|h\|_2\le M. This is the standard device for turning a duality bound |\langle h,g\rangle|\le M\|g\|_2 into a norm bound without knowing beforehand that h lies in L²: each truncation is square-integrable by construction, the displayed inequality reads t_n\le M\sqrt{t_n} for t_n=\|1_{s_n}h\|_2^2, and monotone convergence lifts the resulting uniform bound t_n\le M^2 to h. The auxiliary lintegral form of the L² seminorm — with and without the square root — the natural-power integrability of \|\cdot\|^2, and the inclusion L^1\cap L^\infty\subseteq L^2 (an integrable function with a uniform bound is square-integrable) are provided alongside. So is the lintegral form of Cauchy--Schwarz, \int^-\|u\|_e\|v\|_e\le\|u\|_2\|v\|_2, which needs no integrability hypothesis and allows the two targets to differ, so that it applies to a scalar coefficient paired against a vector-valued kernel.

Lean code for Theorem5.1.6●7 theorems

theoremdefined in LeanRidgelet/ToMathlib/L2Duality.lean

complete

theorem MeasureTheory.eLpNorm_two_eq_lintegral_enorm_sq.{u_1, u_2}
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {E : Type u_2} [NormedAddCommGroup E] (g : α → E) :
  MeasureTheory.eLpNorm g 2 μ = (∫⁻ (x : α), ‖g x‖ₑ ^ 2 ∂μ) ^ (1 / 2)

theorem MeasureTheory.eLpNorm_two_eq_lintegral_enorm_sq.{u_1,
    u_2}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {E : Type u_2} [NormedAddCommGroup E]
  (g : α → E) :
  MeasureTheory.eLpNorm g 2 μ =
    (∫⁻ (x : α), ‖g x‖ₑ ^ 2 ∂μ) ^ (1 / 2)

The `L²` seminorm is the square root of the `lintegral` of the squared enorm.

theoremdefined in LeanRidgelet/ToMathlib/L2Duality.lean

complete

theorem MeasureTheory.eLpNorm_two_sq_eq_lintegral_enorm_sq.{u_1, u_2}
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {F : Type u_2} [NormedAddCommGroup F] (u : α → F) :
  MeasureTheory.eLpNorm u 2 μ ^ 2 = ∫⁻ (a : α), ‖u a‖ₑ ^ 2 ∂μ

theorem MeasureTheory.eLpNorm_two_sq_eq_lintegral_enorm_sq.{u_1,
    u_2}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {F : Type u_2} [NormedAddCommGroup F]
  (u : α → F) :
  MeasureTheory.eLpNorm u 2 μ ^ 2 =
    ∫⁻ (a : α), ‖u a‖ₑ ^ 2 ∂μ

The square of the `L²` seminorm is the lower Lebesgue integral of the squared enorm.  This is
`MeasureTheory.eLpNorm_two_eq_lintegral_enorm_sq` with the square root cleared, which is the form a
caller needs when an `L²` seminorm has to meet a `lintegral` identity.

theoremdefined in LeanRidgelet/ToMathlib/L2Duality.lean

complete

theorem MeasureTheory.lintegral_enorm_mul_le_eLpNorm_two_mul_eLpNorm_two.{u_1,
    u_2, u_3}
  {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α)
  {F : Type u_2} {G : Type u_3} [NormedAddCommGroup F]
  [MeasurableSpace F] [OpensMeasurableSpace F] [NormedAddCommGroup G]
  [MeasurableSpace G] [OpensMeasurableSpace G] {u : α → F} {v : α → G}
  (hu : AEMeasurable u μ) (hv : AEMeasurable v μ) :
  ∫⁻ (a : α), ‖u a‖ₑ * ‖v a‖ₑ ∂μ ≤
    MeasureTheory.eLpNorm u 2 μ * MeasureTheory.eLpNorm v 2 μ

theorem MeasureTheory.lintegral_enorm_mul_le_eLpNorm_two_mul_eLpNorm_two.{u_1,
    u_2, u_3}
  {α : Type u_1} [MeasurableSpace α]
  (μ : MeasureTheory.Measure α)
  {F : Type u_2} {G : Type u_3}
  [NormedAddCommGroup F]
  [MeasurableSpace F]
  [OpensMeasurableSpace F]
  [NormedAddCommGroup G]
  [MeasurableSpace G]
  [OpensMeasurableSpace G] {u : α → F}
  {v : α → G} (hu : AEMeasurable u μ)
  (hv : AEMeasurable v μ) :
  ∫⁻ (a : α), ‖u a‖ₑ * ‖v a‖ₑ ∂μ ≤
    MeasureTheory.eLpNorm u 2 μ *
      MeasureTheory.eLpNorm v 2 μ

**Cauchy--Schwarz for lower Lebesgue integrals.**  The integral of a product of two enorms is at
most the product of the two `L²` seminorms.  This is Hölder's inequality at the conjugate pair
`(2, 2)`, stated for two possibly different targets so that it applies to a pairing of a scalar
coefficient against a vector-valued kernel.

theoremdefined in LeanRidgelet/ToMathlib/L2Duality.lean

complete

theorem MeasureTheory.MemLp.norm_integral_mul_conj_le.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {u v : α → ℂ}
  (hu : MeasureTheory.MemLp u 2 μ) (hv : MeasureTheory.MemLp v 2 μ) :
  ‖∫ (x : α), u x * (starRingEnd ℂ) (v x) ∂μ‖ ≤
    √(∫ (x : α), ‖u x‖ ^ 2 ∂μ) * √(∫ (x : α), ‖v x‖ ^ 2 ∂μ)

theorem MeasureTheory.MemLp.norm_integral_mul_conj_le.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {u v : α → ℂ}
  (hu : MeasureTheory.MemLp u 2 μ)
  (hv : MeasureTheory.MemLp v 2 μ) :
  ‖∫ (x : α),
        u x * (starRingEnd ℂ) (v x) ∂μ‖ ≤
    √(∫ (x : α), ‖u x‖ ^ 2 ∂μ) *
      √(∫ (x : α), ‖v x‖ ^ 2 ∂μ)

**Cauchy--Schwarz inequality** for the Bochner integral of a product `u ⋅ conj v` of
square-integrable scalar functions.

theoremdefined in LeanRidgelet/ToMathlib/L2Duality.lean

complete

theorem MeasureTheory.MemLp.integrable_norm_sq.{u_1, u_2} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {E : Type u_2}
  [NormedAddCommGroup E] {g : α → E} (hg : MeasureTheory.MemLp g 2 μ) :
  MeasureTheory.Integrable (fun x ↦ ‖g x‖ ^ 2) μ

theorem MeasureTheory.MemLp.integrable_norm_sq.{u_1,
    u_2}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {E : Type u_2} [NormedAddCommGroup E]
  {g : α → E}
  (hg : MeasureTheory.MemLp g 2 μ) :
  MeasureTheory.Integrable
    (fun x ↦ ‖g x‖ ^ 2) μ

Square-integrability of the squared norm of an `L²` function, in natural-power form.

theoremdefined in LeanRidgelet/ToMathlib/L2Duality.lean

complete

theorem MeasureTheory.eLpNorm_two_le_of_forall_indicator_pairing_le.{u_1}
  {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α}
  {h : α → ℂ} {M : ℝ} (hM : 0 ≤ M)
  (hh : MeasureTheory.AEStronglyMeasurable h μ) {s : ℕ → Set α}
  (hsm : ∀ (n : ℕ), MeasurableSet (s n)) (hsmono : Monotone s)
  (hsu : ∀ (x : α), ∃ n, x ∈ s n)
  (hmem : ∀ (n : ℕ), MeasureTheory.MemLp ((s n).indicator h) 2 μ)
  (hpair :
    ∀ (n : ℕ),
      ‖∫ (x : α), h x * (starRingEnd ℂ) ((s n).indicator h x) ∂μ‖ ≤
        M * √(∫ (x : α), ‖(s n).indicator h x‖ ^ 2 ∂μ)) :
  MeasureTheory.eLpNorm h 2 μ ≤ ENNReal.ofReal M

theorem MeasureTheory.eLpNorm_two_le_of_forall_indicator_pairing_le.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {h : α → ℂ} {M : ℝ} (hM : 0 ≤ M)
  (hh :
    MeasureTheory.AEStronglyMeasurable h
      μ)
  {s : ℕ → Set α}
  (hsm : ∀ (n : ℕ), MeasurableSet (s n))
  (hsmono : Monotone s)
  (hsu : ∀ (x : α), ∃ n, x ∈ s n)
  (hmem :
    ∀ (n : ℕ),
      MeasureTheory.MemLp
        ((s n).indicator h) 2 μ)
  (hpair :
    ∀ (n : ℕ),
      ‖∫ (x : α),
            h x *
              (starRingEnd ℂ)
                ((s n).indicator h
                  x) ∂μ‖ ≤
        M *
          √(∫ (x : α),
              ‖(s n).indicator h x‖ ^
                2 ∂μ)) :
  MeasureTheory.eLpNorm h 2 μ ≤
    ENNReal.ofReal M

**`L²` duality criterion.** If `h` is measurable, the sets `s n` are measurable, increasing
and exhaust the space, each truncation `1_{s n} h` is square-integrable, and the pairing of `h`
against every truncation is bounded by `M` times the `L²` norm of that truncation, then `h` is
square-integrable with `‖h‖₂ ≤ M`.

theoremdefined in LeanRidgelet/ToMathlib/L2Duality.lean

complete

theorem MeasureTheory.memLp_two_of_integrable_of_bound.{u_1} {α : Type u_1}
  [MeasurableSpace α] {μ : MeasureTheory.Measure α} {h : α → ℂ}
  (hint : MeasureTheory.Integrable h μ) {M : ℝ}
  (hbd : ∀ (x : α), ‖h x‖ ≤ M) : MeasureTheory.MemLp h 2 μ

theorem MeasureTheory.memLp_two_of_integrable_of_bound.{u_1}
  {α : Type u_1} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  {h : α → ℂ}
  (hint : MeasureTheory.Integrable h μ)
  {M : ℝ} (hbd : ∀ (x : α), ‖h x‖ ≤ M) :
  MeasureTheory.MemLp h 2 μ

An integrable function with a uniform bound is square-integrable.

Theorem5.1.7

uses 0used by 1✓L∃∀N

Measurability of an iterated derivative in a parameter. Mathlib knows that a single derivative is measurable with no differentiability assumption — for one variable because the derivative vanishes off the differentiability set and that set is Borel, and for a jointly continuous family by the same argument with a parameter — but neither statement iterates on its own, the parametric one consuming a joint continuity it does not produce. One variable is then free: iterating costs nothing, so an iterated derivative of positive order is strongly measurable for every function on the line. A parameter has content, and there are two routes. The continuity route supplies the missing induction: the derivative in the last variable of a jointly C^{m+1} function of a pair is jointly C^m, so an induction on the order gives joint continuity of the parametric iterated derivative. Feeding that back into the one-step lemma gains an order, so C^j gives measurability of order j+1 rather than of order j. The limit route is the one-step lemma itself, stated in this file's notation: joint continuity at order j gives joint measurability at order j+1, assuming no differentiability at all.

Lean code for Theorem5.1.7●15 declarations

theoremdefined in LeanRidgelet/ToMathlib/ParametricIteratedDeriv.lean

complete

theorem MeasureTheory.stronglyMeasurable_iteratedDeriv_succ.{u_1} {F : Type u_1}
  [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (j : ℕ)
  (g : ℝ → F) :
  MeasureTheory.StronglyMeasurable (iteratedDeriv (j + 1) g)

theorem MeasureTheory.stronglyMeasurable_iteratedDeriv_succ.{u_1}
  {F : Type u_1} [NormedAddCommGroup F]
  [NormedSpace ℝ F] [CompleteSpace F]
  (j : ℕ) (g : ℝ → F) :
  MeasureTheory.StronglyMeasurable
    (iteratedDeriv (j + 1) g)

**An iterated derivative of positive order is strongly measurable, unconditionally.**  For every
function on the line into a complete space, differentiable or not, the `(j + 1)`-st iterated
derivative is strongly measurable.  Only Mathlib's `MeasureTheory.stronglyMeasurable_deriv` is used:
the derivative vanishes off the differentiability set, which is Borel, so no regularity of `g` is
needed, and `iteratedDeriv (j + 1) g = deriv (iteratedDeriv j g)` iterates that for free.  Order `0`
is the only order that needs a hypothesis, since there the iterated derivative is `g` itself.

theoremdefined in LeanRidgelet/ToMathlib/ParametricIteratedDeriv.lean

complete

theorem MeasureTheory.stronglyMeasurable_iteratedDeriv.{u_1} {F : Type u_1}
  [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (j : ℕ)
  {g : ℝ → F} (hg : MeasureTheory.StronglyMeasurable g) :
  MeasureTheory.StronglyMeasurable (iteratedDeriv j g)

theorem MeasureTheory.stronglyMeasurable_iteratedDeriv.{u_1}
  {F : Type u_1} [NormedAddCommGroup F]
  [NormedSpace ℝ F] [CompleteSpace F]
  (j : ℕ) {g : ℝ → F}
  (hg :
    MeasureTheory.StronglyMeasurable g) :
  MeasureTheory.StronglyMeasurable
    (iteratedDeriv j g)

Every iterated derivative of a strongly measurable function is strongly measurable.  For a
positive order the hypothesis is not used; it is needed only at order `0`.

defdefined in LeanRidgelet/ToMathlib/ParametricIteratedDeriv.lean

complete

def MeasureTheory.parametricDeriv.{u_1, u_2} {α : Type u_1} {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℝ F] (f : α × ℝ → F) : α × ℝ → F

def MeasureTheory.parametricDeriv.{u_1, u_2}
  {α : Type u_1} {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  (f : α × ℝ → F) : α × ℝ → F

Implementation after :=

:=
  fun p ↦ deriv (fun t ↦ f (p.1, t)) p.2

**The parametric derivative.**  The derivative in the last variable of a function of a pair,
read again as a function of the pair.  The first component is the parameter and is not
differentiated.

defdefined in LeanRidgelet/ToMathlib/ParametricIteratedDeriv.lean

complete

def MeasureTheory.parametricIteratedDeriv.{u_1, u_2} {α : Type u_1}
  {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (j : ℕ)
  (f : α × ℝ → F) : α × ℝ → F

def MeasureTheory.parametricIteratedDeriv.{u_1,
    u_2}
  {α : Type u_1} {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  (j : ℕ) (f : α × ℝ → F) : α × ℝ → F

Implementation after :=

:=
  fun p ↦ iteratedDeriv j (fun t ↦ f (p.1, t)) p.2

**The parametric iterated derivative.**  The `j`-th derivative in the last variable of a
function of a pair, read again as a function of the pair.  This is the shape of
`LeanRidgelet.quadraticConstIteratedDeriv`, up to the reassociation of the parameter space handled
below.

theoremdefined in LeanRidgelet/ToMathlib/ParametricIteratedDeriv.lean

complete

theorem MeasureTheory.parametricDeriv_slice.{u_1, u_2} {α : Type u_1}
  {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F]
  (f : α × ℝ → F) (a : α) :
  (fun t ↦ MeasureTheory.parametricDeriv f (a, t)) =
    deriv fun t ↦ f (a, t)

theorem MeasureTheory.parametricDeriv_slice.{u_1,
    u_2}
  {α : Type u_1} {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  (f : α × ℝ → F) (a : α) :
  (fun t ↦
      MeasureTheory.parametricDeriv f
        (a, t)) =
    deriv fun t ↦ f (a, t)

A slice of the parametric derivative is the derivative of the slice.  This holds by
definition.

theoremdefined in LeanRidgelet/ToMathlib/ParametricIteratedDeriv.lean

complete

theorem MeasureTheory.parametricIteratedDeriv_slice.{u_1, u_2} {α : Type u_1}
  {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (j : ℕ)
  (f : α × ℝ → F) (a : α) :
  (fun t ↦ MeasureTheory.parametricIteratedDeriv j f (a, t)) =
    iteratedDeriv j fun t ↦ f (a, t)

theorem MeasureTheory.parametricIteratedDeriv_slice.{u_1,
    u_2}
  {α : Type u_1} {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  (j : ℕ) (f : α × ℝ → F) (a : α) :
  (fun t ↦
      MeasureTheory.parametricIteratedDeriv
        j f (a, t)) =
    iteratedDeriv j fun t ↦ f (a, t)

A slice of the parametric iterated derivative is the iterated derivative of the slice.  This
holds by definition, and it is the bridge between statements about the pair and slice-wise
statements.

theoremdefined in LeanRidgelet/ToMathlib/ParametricIteratedDeriv.lean

complete

theorem MeasureTheory.parametricIteratedDeriv_zero.{u_1, u_2} {α : Type u_1}
  {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F]
  (f : α × ℝ → F) : MeasureTheory.parametricIteratedDeriv 0 f = f

theorem MeasureTheory.parametricIteratedDeriv_zero.{u_1,
    u_2}
  {α : Type u_1} {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  (f : α × ℝ → F) :
  MeasureTheory.parametricIteratedDeriv 0
      f =
    f

The parametric iterated derivative of order zero is the function itself.

theoremdefined in LeanRidgelet/ToMathlib/ParametricIteratedDeriv.lean

complete

theorem MeasureTheory.parametricIteratedDeriv_succ.{u_1, u_2} {α : Type u_1}
  {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (j : ℕ)
  (f : α × ℝ → F) :
  MeasureTheory.parametricIteratedDeriv (j + 1) f =
    MeasureTheory.parametricIteratedDeriv j
      (MeasureTheory.parametricDeriv f)

theorem MeasureTheory.parametricIteratedDeriv_succ.{u_1,
    u_2}
  {α : Type u_1} {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  (j : ℕ) (f : α × ℝ → F) :
  MeasureTheory.parametricIteratedDeriv
      (j + 1) f =
    MeasureTheory.parametricIteratedDeriv
      j (MeasureTheory.parametricDeriv f)

**Peeling off the innermost derivative.**  The parametric iterated derivative of order `j + 1`
is the one of order `j` of the parametric derivative.  This is the recursion the continuity route
descends.

theoremdefined in LeanRidgelet/ToMathlib/ParametricIteratedDeriv.lean

complete

theorem MeasureTheory.parametricIteratedDeriv_succ'.{u_1, u_2} {α : Type u_1}
  {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] (j : ℕ)
  (f : α × ℝ → F) :
  MeasureTheory.parametricIteratedDeriv (j + 1) f =
    MeasureTheory.parametricDeriv
      (MeasureTheory.parametricIteratedDeriv j f)

theorem MeasureTheory.parametricIteratedDeriv_succ'.{u_1,
    u_2}
  {α : Type u_1} {F : Type u_2}
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  (j : ℕ) (f : α × ℝ → F) :
  MeasureTheory.parametricIteratedDeriv
      (j + 1) f =
    MeasureTheory.parametricDeriv
      (MeasureTheory.parametricIteratedDeriv
        j f)

**Peeling off the outermost derivative.**  The parametric iterated derivative of order `j + 1`
is the parametric derivative of the one of order `j`.  This is the recursion the limit route uses,
since Mathlib's parametric statement is about a single derivative of a jointly continuous family.

theoremdefined in LeanRidgelet/ToMathlib/ParametricIteratedDeriv.lean

complete

theorem MeasureTheory.measurable_parametricDeriv_of_continuous.{u_1, u_2}
  {α : Type u_1} {F : Type u_2} [TopologicalSpace α] [MeasurableSpace α]
  [OpensMeasurableSpace α] [NormedAddCommGroup F] [NormedSpace ℝ F]
  [CompleteSpace F] [MeasurableSpace F] [BorelSpace F] {f : α × ℝ → F}
  (hf : Continuous f) : Measurable (MeasureTheory.parametricDeriv f)

theorem MeasureTheory.measurable_parametricDeriv_of_continuous.{u_1,
    u_2}
  {α : Type u_1} {F : Type u_2}
  [TopologicalSpace α] [MeasurableSpace α]
  [OpensMeasurableSpace α]
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  [CompleteSpace F] [MeasurableSpace F]
  [BorelSpace F] {f : α × ℝ → F}
  (hf : Continuous f) :
  Measurable
    (MeasureTheory.parametricDeriv f)

**One parametric derivative of a jointly continuous function is jointly measurable.**  This is
Mathlib's `measurable_deriv_with_param` in the notation of this file, and it is the sharp form of
the limit route: the parametric derivative is a pointwise limit of difference quotients, so no
differentiability is needed anywhere, only joint continuity.  What it does not do is iterate, since
joint continuity of the derivative is not part of its conclusion.

theoremdefined in LeanRidgelet/ToMathlib/ParametricIteratedDeriv.lean

complete

theorem MeasureTheory.measurable_parametricIteratedDeriv_succ_of_continuous.{u_1,
    u_2}
  {α : Type u_1} {F : Type u_2} [TopologicalSpace α] [MeasurableSpace α]
  [OpensMeasurableSpace α] [NormedAddCommGroup F] [NormedSpace ℝ F]
  [CompleteSpace F] [MeasurableSpace F] [BorelSpace F] {j : ℕ}
  {f : α × ℝ → F}
  (hf : Continuous (MeasureTheory.parametricIteratedDeriv j f)) :
  Measurable (MeasureTheory.parametricIteratedDeriv (j + 1) f)

theorem MeasureTheory.measurable_parametricIteratedDeriv_succ_of_continuous.{u_1,
    u_2}
  {α : Type u_1} {F : Type u_2}
  [TopologicalSpace α] [MeasurableSpace α]
  [OpensMeasurableSpace α]
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  [CompleteSpace F] [MeasurableSpace F]
  [BorelSpace F] {j : ℕ} {f : α × ℝ → F}
  (hf :
    Continuous
      (MeasureTheory.parametricIteratedDeriv
        j f)) :
  Measurable
    (MeasureTheory.parametricIteratedDeriv
      (j + 1) f)

**The limit route, one order up.**  If the parametric iterated derivative of order `j` is
jointly continuous, then the one of order `j + 1` is jointly measurable.  This gains one order over
what continuity alone would give, and needs no differentiability.

theoremdefined in LeanRidgelet/ToMathlib/ParametricIteratedDeriv.lean

complete

theorem MeasureTheory.contDiff_parametricDeriv.{u_1, u_2} {α : Type u_1}
  {F : Type u_2} [NormedAddCommGroup α] [NormedSpace ℝ α]
  [NormedAddCommGroup F] [NormedSpace ℝ F] {m : WithTop ℕ∞}
  {f : α × ℝ → F} (hf : ContDiff ℝ (m + 1) f) :
  ContDiff ℝ m (MeasureTheory.parametricDeriv f)

theorem MeasureTheory.contDiff_parametricDeriv.{u_1,
    u_2}
  {α : Type u_1} {F : Type u_2}
  [NormedAddCommGroup α] [NormedSpace ℝ α]
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  {m : WithTop ℕ∞} {f : α × ℝ → F}
  (hf : ContDiff ℝ (m + 1) f) :
  ContDiff ℝ m
    (MeasureTheory.parametricDeriv f)

**The parametric derivative of a jointly smooth function is jointly smooth, one order down.**
The derivative in the last variable is the full derivative in the pair, evaluated at the last basis
covector, so `ContDiff.fderiv_succ` gives it directly; evaluation at `1` is a continuous linear map,
which costs no smoothness.  Nothing is assumed about how the two variables interact.

theoremdefined in LeanRidgelet/ToMathlib/ParametricIteratedDeriv.lean

complete

theorem MeasureTheory.continuous_parametricIteratedDeriv.{u_1, u_2}
  {α : Type u_1} {F : Type u_2} [NormedAddCommGroup α] [NormedSpace ℝ α]
  [NormedAddCommGroup F] [NormedSpace ℝ F] {j : ℕ} {f : α × ℝ → F}
  (hf : ContDiff ℝ (↑j) f) :
  Continuous (MeasureTheory.parametricIteratedDeriv j f)

theorem MeasureTheory.continuous_parametricIteratedDeriv.{u_1,
    u_2}
  {α : Type u_1} {F : Type u_2}
  [NormedAddCommGroup α] [NormedSpace ℝ α]
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  {j : ℕ} {f : α × ℝ → F}
  (hf : ContDiff ℝ (↑j) f) :
  Continuous
    (MeasureTheory.parametricIteratedDeriv
      j f)

**The continuity route.**  For a function of a pair that is `j` times continuously
differentiable in the pair, the `j`-th derivative in the last variable is jointly continuous in the
pair.  The induction descends `LeanRidgelet.parametricIteratedDeriv_succ`, spending one order of
smoothness per derivative and reading off continuity from `ContDiff ℝ 0` at the end.

This is the honest general form of "the parametric iterated derivative is continuous, hence
measurable": the hypothesis is joint smoothness, which is what a concrete ridgelet function built
from a smooth activation has, and there is no differentiability side condition to check, since
`ContDiff` supplies it.

theoremdefined in LeanRidgelet/ToMathlib/ParametricIteratedDeriv.lean

complete

theorem MeasureTheory.measurable_parametricIteratedDeriv.{u_1, u_2}
  {α : Type u_1} {F : Type u_2} [NormedAddCommGroup α] [NormedSpace ℝ α]
  [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace α]
  [OpensMeasurableSpace α] [MeasurableSpace F] [BorelSpace F] {j : ℕ}
  {f : α × ℝ → F} (hf : ContDiff ℝ (↑j) f) :
  Measurable (MeasureTheory.parametricIteratedDeriv j f)

theorem MeasureTheory.measurable_parametricIteratedDeriv.{u_1,
    u_2}
  {α : Type u_1} {F : Type u_2}
  [NormedAddCommGroup α] [NormedSpace ℝ α]
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  [MeasurableSpace α]
  [OpensMeasurableSpace α]
  [MeasurableSpace F] [BorelSpace F]
  {j : ℕ} {f : α × ℝ → F}
  (hf : ContDiff ℝ (↑j) f) :
  Measurable
    (MeasureTheory.parametricIteratedDeriv
      j f)

**The continuity route, as measurability.**  Joint continuity of the parametric iterated
derivative makes it measurable for the Borel structure of the pair.

theoremdefined in LeanRidgelet/ToMathlib/ParametricIteratedDeriv.lean

complete

theorem MeasureTheory.measurable_parametricIteratedDeriv_succ.{u_1, u_2}
  {α : Type u_1} {F : Type u_2} [NormedAddCommGroup α] [NormedSpace ℝ α]
  [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace α]
  [OpensMeasurableSpace α] [MeasurableSpace F] [BorelSpace F]
  [CompleteSpace F] {j : ℕ} {f : α × ℝ → F} (hf : ContDiff ℝ (↑j) f) :
  Measurable (MeasureTheory.parametricIteratedDeriv (j + 1) f)

theorem MeasureTheory.measurable_parametricIteratedDeriv_succ.{u_1,
    u_2}
  {α : Type u_1} {F : Type u_2}
  [NormedAddCommGroup α] [NormedSpace ℝ α]
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  [MeasurableSpace α]
  [OpensMeasurableSpace α]
  [MeasurableSpace F] [BorelSpace F]
  [CompleteSpace F] {j : ℕ}
  {f : α × ℝ → F}
  (hf : ContDiff ℝ (↑j) f) :
  Measurable
    (MeasureTheory.parametricIteratedDeriv
      (j + 1) f)

**The two routes combined.**  `j` orders of joint smoothness give joint measurability of the
parametric iterated derivative of order `j + 1`: the first `j` derivatives are continuous by the
continuity route, and the last one is measurable by Mathlib's parametric statement, which needs only
continuity of the previous one.  At `j = 0` this says that joint continuity of `f` alone makes the
parametric first derivative measurable.

Theorem5.1.8

uses 0used by 0✓L∃∀N

A bounded operator on L^2 from a pointwise formula. An integral transform is given by a formula on functions; turning it into a bounded operator is always the same four steps, and this does them once.

Lean code for Theorem5.1.8●6 declarations

defdefined in LeanRidgelet/ToMathlib/LpOperatorOfPointwise.lean

complete

def MeasureTheory.lpLinearMapOfPointwise.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  {T : (α → ℂ) → β → ℂ}
  (hmem :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)), MeasureTheory.MemLp (T ↑↑f) 2 ν)
  (hadd :
    ∀ (f g : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(f + g) =ᵐ[ν] T ↑↑f + T ↑↑g)
  (hsmul :
    ∀ (c : ℂ) (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(c • f) =ᵐ[ν] c • T ↑↑f) :
  ↥(MeasureTheory.Lp ℂ 2 μ) →ₗ[ℂ] ↥(MeasureTheory.Lp ℂ 2 ν)

def MeasureTheory.lpLinearMapOfPointwise.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  {T : (α → ℂ) → β → ℂ}
  (hmem :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      MeasureTheory.MemLp (T ↑↑f) 2 ν)
  (hadd :
    ∀ (f g : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(f + g) =ᵐ[ν] T ↑↑f + T ↑↑g)
  (hsmul :
    ∀ (c : ℂ)
      (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(c • f) =ᵐ[ν] c • T ↑↑f) :
  ↥(MeasureTheory.Lp ℂ 2 μ) →ₗ[ℂ]
    ↥(MeasureTheory.Lp ℂ 2 ν)

Implementation after :=

:= (hmem f).toLp _
  map_add' f g := by
    refine Lp.ext_iff.2 ?_
    filter_upwards [MemLp.coeFn_toLp (hmem (f + g)),
      Lp.coeFn_add ((hmem f).toLp (T (f : α → ℂ))) ((hmem g).toLp (T (g : α → ℂ))),
      MemLp.coeFn_toLp (hmem f), MemLp.coeFn_toLp (hmem g), hadd f g] with x h1 h2 h3 h4 h5
    rw [h1, h2, Pi.add_apply, h3, h4, h5, Pi.add_apply]
  map_smul' c f := by
    refine Lp.ext_iff.2 ?_
    filter_upwards [MemLp.coeFn_toLp (hmem (c • f)),
      Lp.coeFn_smul c ((hmem f).toLp (T (f : α → ℂ))),
      MemLp.coeFn_toLp (hmem f), hsmul c f] with x h1 h2 h3 h4
    simp only [RingHom.id_apply]
    rw [h1, h2, Pi.smul_apply, h3, h4, Pi.smul_apply]

The linear map underlying `MeasureTheory.lpOperatorOfPointwise`.  Additivity and homogeneity are
the hypotheses, taken almost everywhere, since that is the level at which an `L²` class determines
its representative.

theoremdefined in LeanRidgelet/ToMathlib/LpOperatorOfPointwise.lean

complete

theorem MeasureTheory.coeFn_lpLinearMapOfPointwise.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  {T : (α → ℂ) → β → ℂ}
  (hmem :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)), MeasureTheory.MemLp (T ↑↑f) 2 ν)
  (hadd :
    ∀ (f g : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(f + g) =ᵐ[ν] T ↑↑f + T ↑↑g)
  (hsmul :
    ∀ (c : ℂ) (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(c • f) =ᵐ[ν] c • T ↑↑f)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ)) :
  ↑↑((MeasureTheory.lpLinearMapOfPointwise hmem hadd hsmul) f) =ᵐ[ν]
    T ↑↑f

theorem MeasureTheory.coeFn_lpLinearMapOfPointwise.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  {T : (α → ℂ) → β → ℂ}
  (hmem :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      MeasureTheory.MemLp (T ↑↑f) 2 ν)
  (hadd :
    ∀ (f g : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(f + g) =ᵐ[ν] T ↑↑f + T ↑↑g)
  (hsmul :
    ∀ (c : ℂ)
      (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(c • f) =ᵐ[ν] c • T ↑↑f)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ)) :
  ↑↑((MeasureTheory.lpLinearMapOfPointwise
            hmem hadd hsmul)
          f) =ᵐ[ν]
    T ↑↑f

defdefined in LeanRidgelet/ToMathlib/LpOperatorOfPointwise.lean

complete

def MeasureTheory.lpOperatorOfPointwise.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  {T : (α → ℂ) → β → ℂ} {C : ℝ} (_hC : 0 ≤ C)
  (hmem :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)), MeasureTheory.MemLp (T ↑↑f) 2 ν)
  (hadd :
    ∀ (f g : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(f + g) =ᵐ[ν] T ↑↑f + T ↑↑g)
  (hsmul :
    ∀ (c : ℂ) (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(c • f) =ᵐ[ν] c • T ↑↑f)
  (hbound :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      (MeasureTheory.eLpNorm (T ↑↑f) 2 ν).toReal ≤ C * ‖f‖) :
  ↥(MeasureTheory.Lp ℂ 2 μ) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 ν)

def MeasureTheory.lpOperatorOfPointwise.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  {T : (α → ℂ) → β → ℂ} {C : ℝ}
  (_hC : 0 ≤ C)
  (hmem :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      MeasureTheory.MemLp (T ↑↑f) 2 ν)
  (hadd :
    ∀ (f g : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(f + g) =ᵐ[ν] T ↑↑f + T ↑↑g)
  (hsmul :
    ∀ (c : ℂ)
      (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(c • f) =ᵐ[ν] c • T ↑↑f)
  (hbound :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      (MeasureTheory.eLpNorm (T ↑↑f) 2
            ν).toReal ≤
        C * ‖f‖) :
  ↥(MeasureTheory.Lp ℂ 2 μ) →L[ℂ]
    ↥(MeasureTheory.Lp ℂ 2 ν)

Implementation after :=

:=
  LinearMap.mkContinuous (lpLinearMapOfPointwise hmem hadd hsmul) C fun f ↦ by
    have h : ‖lpLinearMapOfPointwise hmem hadd hsmul f‖ = (eLpNorm (T (f : α → ℂ)) 2 ν).toReal :=
      Lp.norm_toLp _ (hmem f)
    rw [h]
    exact hbound f

**A bounded operator on `L²` from a pointwise formula.**  Given that the formula's value is
square integrable, that it is additive and homogeneous almost everywhere, and that its `L²` norm is
at most a constant times the input's, the formula defines a bounded linear operator between the `L²`
spaces.

The four hypotheses are what an integral transform supplies: square integrability and the norm
bound come from an estimate on the transform, and additivity and homogeneity come from integrability
of the defining integral, which is what lets it be split.

theoremdefined in LeanRidgelet/ToMathlib/LpOperatorOfPointwise.lean

complete

theorem MeasureTheory.lpOperatorOfPointwise_apply.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  {T : (α → ℂ) → β → ℂ} {C : ℝ} (hC : 0 ≤ C)
  (hmem :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)), MeasureTheory.MemLp (T ↑↑f) 2 ν)
  (hadd :
    ∀ (f g : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(f + g) =ᵐ[ν] T ↑↑f + T ↑↑g)
  (hsmul :
    ∀ (c : ℂ) (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(c • f) =ᵐ[ν] c • T ↑↑f)
  (hbound :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      (MeasureTheory.eLpNorm (T ↑↑f) 2 ν).toReal ≤ C * ‖f‖)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ)) :
  (MeasureTheory.lpOperatorOfPointwise hC hmem hadd hsmul hbound) f =
    (MeasureTheory.lpLinearMapOfPointwise hmem hadd hsmul) f

theorem MeasureTheory.lpOperatorOfPointwise_apply.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  {T : (α → ℂ) → β → ℂ} {C : ℝ}
  (hC : 0 ≤ C)
  (hmem :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      MeasureTheory.MemLp (T ↑↑f) 2 ν)
  (hadd :
    ∀ (f g : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(f + g) =ᵐ[ν] T ↑↑f + T ↑↑g)
  (hsmul :
    ∀ (c : ℂ)
      (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(c • f) =ᵐ[ν] c • T ↑↑f)
  (hbound :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      (MeasureTheory.eLpNorm (T ↑↑f) 2
            ν).toReal ≤
        C * ‖f‖)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ)) :
  (MeasureTheory.lpOperatorOfPointwise hC
        hmem hadd hsmul hbound)
      f =
    (MeasureTheory.lpLinearMapOfPointwise
        hmem hadd hsmul)
      f

theoremdefined in LeanRidgelet/ToMathlib/LpOperatorOfPointwise.lean

complete

theorem MeasureTheory.coeFn_lpOperatorOfPointwise.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  {T : (α → ℂ) → β → ℂ} {C : ℝ} (hC : 0 ≤ C)
  (hmem :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)), MeasureTheory.MemLp (T ↑↑f) 2 ν)
  (hadd :
    ∀ (f g : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(f + g) =ᵐ[ν] T ↑↑f + T ↑↑g)
  (hsmul :
    ∀ (c : ℂ) (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(c • f) =ᵐ[ν] c • T ↑↑f)
  (hbound :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      (MeasureTheory.eLpNorm (T ↑↑f) 2 ν).toReal ≤ C * ‖f‖)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ)) :
  ↑↑((MeasureTheory.lpOperatorOfPointwise hC hmem hadd hsmul hbound)
          f) =ᵐ[ν]
    T ↑↑f

theorem MeasureTheory.coeFn_lpOperatorOfPointwise.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  {T : (α → ℂ) → β → ℂ} {C : ℝ}
  (hC : 0 ≤ C)
  (hmem :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      MeasureTheory.MemLp (T ↑↑f) 2 ν)
  (hadd :
    ∀ (f g : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(f + g) =ᵐ[ν] T ↑↑f + T ↑↑g)
  (hsmul :
    ∀ (c : ℂ)
      (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(c • f) =ᵐ[ν] c • T ↑↑f)
  (hbound :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      (MeasureTheory.eLpNorm (T ↑↑f) 2
            ν).toReal ≤
        C * ‖f‖)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ)) :
  ↑↑((MeasureTheory.lpOperatorOfPointwise
            hC hmem hadd hsmul hbound)
          f) =ᵐ[ν]
    T ↑↑f

The operator's values are represented by the formula.

theoremdefined in LeanRidgelet/ToMathlib/LpOperatorOfPointwise.lean

complete

theorem MeasureTheory.norm_lpOperatorOfPointwise_le.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  {T : (α → ℂ) → β → ℂ} {C : ℝ} (hC : 0 ≤ C)
  (hmem :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)), MeasureTheory.MemLp (T ↑↑f) 2 ν)
  (hadd :
    ∀ (f g : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(f + g) =ᵐ[ν] T ↑↑f + T ↑↑g)
  (hsmul :
    ∀ (c : ℂ) (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(c • f) =ᵐ[ν] c • T ↑↑f)
  (hbound :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      (MeasureTheory.eLpNorm (T ↑↑f) 2 ν).toReal ≤ C * ‖f‖) :
  ‖MeasureTheory.lpOperatorOfPointwise hC hmem hadd hsmul hbound‖ ≤ C

theorem MeasureTheory.norm_lpOperatorOfPointwise_le.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  {T : (α → ℂ) → β → ℂ} {C : ℝ}
  (hC : 0 ≤ C)
  (hmem :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      MeasureTheory.MemLp (T ↑↑f) 2 ν)
  (hadd :
    ∀ (f g : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(f + g) =ᵐ[ν] T ↑↑f + T ↑↑g)
  (hsmul :
    ∀ (c : ℂ)
      (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      T ↑↑(c • f) =ᵐ[ν] c • T ↑↑f)
  (hbound :
    ∀ (f : ↥(MeasureTheory.Lp ℂ 2 μ)),
      (MeasureTheory.eLpNorm (T ↑↑f) 2
            ν).toReal ≤
        C * ‖f‖) :
  ‖MeasureTheory.lpOperatorOfPointwise hC
        hmem hadd hsmul hbound‖ ≤
    C

The operator norm is at most the constant of the bound.

The four inputs are: the formula's value is square integrable, the formula is additive and homogeneous almost everywhere, and its L^2 norm is at most a constant times the input's. Out comes the operator, with its values represented by the formula and its operator norm bounded by that constant.

Additivity and homogeneity are hypotheses rather than consequences, and that is the point of the packaging. A formula linear on functions need not be linear on almost-everywhere classes: splitting the defining integral over a sum requires each piece to be integrable. So those two hypotheses are exactly where the integrability of an integral transform enters, and isolating them is what makes the rest mechanical.

Theorem5.1.9

uses 0

Used by 4

Reverse dependency previews

Preview

Theorem 4.1.6

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Pointwise representatives of L²-valued Bochner integrals. Let \Phi(a) be a scalar L² class with representatives F(a,b). If \Phi is Bochner integrable and F is integrable on the product measure, then \left(\int \Phi(a)\,d\mu(a)\right)(b)=\int F(a,b)\,d\mu(a) for almost every b. The proof tests both sides against indicators of arbitrary finite-measure sets. The resulting L² inner-product functional commutes with the Bochner integral, and Fubini identifies the two set integrals. This is the bridge from an L²-valued integrated representation to a pointwise convolution representative.

Lean code for Theorem5.1.9●4 theorems

theoremdefined in LeanRidgelet/ToMathlib/BochnerIntegralL2.lean

complete

theorem MeasureTheory.integral_L2_coeFn_ae.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {𝕜 : Type u_3} [MeasurableSpace α] [MeasurableSpace β]
  [RCLike 𝕜] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν]
  {φ : α → ↥(MeasureTheory.Lp 𝕜 2 ν)} {F : α → β → 𝕜}
  (hφ : MeasureTheory.Integrable φ μ)
  (hF : MeasureTheory.Integrable (Function.uncurry F) (μ.prod ν))
  (hφF : ∀ᵐ (a : α) ∂μ, ↑↑(φ a) =ᵐ[ν] F a) :
  ↑↑(∫ (a : α), φ a ∂μ) =ᵐ[ν] fun b ↦ ∫ (a : α), F a b ∂μ

theorem MeasureTheory.integral_L2_coeFn_ae.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {𝕜 : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] [RCLike 𝕜]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  {φ : α → ↥(MeasureTheory.Lp 𝕜 2 ν)}
  {F : α → β → 𝕜}
  (hφ : MeasureTheory.Integrable φ μ)
  (hF :
    MeasureTheory.Integrable
      (Function.uncurry F) (μ.prod ν))
  (hφF :
    ∀ᵐ (a : α) ∂μ, ↑↑(φ a) =ᵐ[ν] F a) :
  ↑↑(∫ (a : α), φ a ∂μ) =ᵐ[ν] fun b ↦
    ∫ (a : α), F a b ∂μ

theoremdefined in LeanRidgelet/ToMathlib/BochnerIntegralL2.lean

complete

theorem MeasureTheory.integral_L2_coeFn_ae_of_restrict_of_aefinStronglyMeasurable.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2} {𝕜 : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] [RCLike 𝕜] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] {φ : α → ↥(MeasureTheory.Lp 𝕜 2 ν)}
  {F : α → β → 𝕜} (hφ : MeasureTheory.Integrable φ μ)
  (hF :
    ∀ (s : Set β),
      MeasurableSet s →
        ν s ≠ ⊤ →
          MeasureTheory.Integrable (Function.uncurry F)
            (μ.prod (ν.restrict s)))
  (hmeas :
    MeasureTheory.AEFinStronglyMeasurable (fun b ↦ ∫ (a : α), F a b ∂μ)
      ν)
  (hφF : ∀ᵐ (a : α) ∂μ, ↑↑(φ a) =ᵐ[ν] F a) :
  ↑↑(∫ (a : α), φ a ∂μ) =ᵐ[ν] fun b ↦ ∫ (a : α), F a b ∂μ

theorem MeasureTheory.integral_L2_coeFn_ae_of_restrict_of_aefinStronglyMeasurable.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {𝕜 : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] [RCLike 𝕜]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  {φ : α → ↥(MeasureTheory.Lp 𝕜 2 ν)}
  {F : α → β → 𝕜}
  (hφ : MeasureTheory.Integrable φ μ)
  (hF :
    ∀ (s : Set β),
      MeasurableSet s →
        ν s ≠ ⊤ →
          MeasureTheory.Integrable
            (Function.uncurry F)
            (μ.prod (ν.restrict s)))
  (hmeas :
    MeasureTheory.AEFinStronglyMeasurable
      (fun b ↦ ∫ (a : α), F a b ∂μ) ν)
  (hφF :
    ∀ᵐ (a : α) ∂μ, ↑↑(φ a) =ᵐ[ν] F a) :
  ↑↑(∫ (a : α), φ a ∂μ) =ᵐ[ν] fun b ↦
    ∫ (a : α), F a b ∂μ

A Bochner integral in scalar `L²` has the pointwise iterated integral as an almost-everywhere
representative when the chosen two-variable representatives are integrable over every slice
`μ.prod (ν.restrict s)` with `ν s < ∞`.

This is the form in which the finite-measure test sets are used: equality is detected by
integrating over every measurable set of finite measure, using its indicator as an `L²` test
vector, and only integrability over that set is needed to commute the two integrals. The
almost-everywhere fin-strong measurability of the pointwise integral, which the slice hypothesis
cannot supply, is assumed separately.

theoremdefined in LeanRidgelet/ToMathlib/BochnerIntegralL2.lean

complete

theorem MeasureTheory.integral_L2_coeFn_ae_of_restrict.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {𝕜 : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] [RCLike 𝕜] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ]
  [MeasureTheory.SigmaFinite ν] {φ : α → ↥(MeasureTheory.Lp 𝕜 2 ν)}
  {F : α → β → 𝕜} (hφ : MeasureTheory.Integrable φ μ)
  (hF :
    ∀ (s : Set β),
      MeasurableSet s →
        ν s ≠ ⊤ →
          MeasureTheory.Integrable (Function.uncurry F)
            (μ.prod (ν.restrict s)))
  (hmeas :
    MeasureTheory.AEStronglyMeasurable (fun b ↦ ∫ (a : α), F a b ∂μ) ν)
  (hφF : ∀ᵐ (a : α) ∂μ, ↑↑(φ a) =ᵐ[ν] F a) :
  ↑↑(∫ (a : α), φ a ∂μ) =ᵐ[ν] fun b ↦ ∫ (a : α), F a b ∂μ

theorem MeasureTheory.integral_L2_coeFn_ae_of_restrict.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {𝕜 : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] [RCLike 𝕜]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SigmaFinite ν]
  {φ : α → ↥(MeasureTheory.Lp 𝕜 2 ν)}
  {F : α → β → 𝕜}
  (hφ : MeasureTheory.Integrable φ μ)
  (hF :
    ∀ (s : Set β),
      MeasurableSet s →
        ν s ≠ ⊤ →
          MeasureTheory.Integrable
            (Function.uncurry F)
            (μ.prod (ν.restrict s)))
  (hmeas :
    MeasureTheory.AEStronglyMeasurable
      (fun b ↦ ∫ (a : α), F a b ∂μ) ν)
  (hφF :
    ∀ᵐ (a : α) ∂μ, ↑↑(φ a) =ᵐ[ν] F a) :
  ↑↑(∫ (a : α), φ a ∂μ) =ᵐ[ν] fun b ↦
    ∫ (a : α), F a b ∂μ

A Bochner integral in scalar `L²` has the pointwise iterated integral as an almost-everywhere
representative when the chosen two-variable representatives are integrable over every slice
`μ.prod (ν.restrict s)` with `ν s < ∞`.

Unlike `MeasureTheory.integral_L2_coeFn_ae`, the family `F` need not be integrable on all of
`μ.prod ν`, so a merely locally integrable pointwise integral is allowed; the price is that the
measurability of `fun b ↦ ∫ a, F a b ∂μ` must be assumed, and that `ν` must be σ-finite for that
measurability to give the fin-strong measurability the test-set criterion consumes.

theoremdefined in LeanRidgelet/ToMathlib/BochnerIntegralL2.lean

complete

theorem MeasureTheory.integral_norm_restrict_le_norm_mul_rpow.{u_1, u_2}
  {α : Type u_1} {F : Type u_2} [MeasurableSpace α]
  [NormedAddCommGroup F] (μ : MeasureTheory.Measure α) {s : Set α}
  (hs : MeasurableSet s) (hfin : μ s ≠ ⊤)
  (h : ↥(MeasureTheory.Lp F 2 μ)) :
  ∫ (a : α) in s, ‖↑↑h a‖ ∂μ ≤ ‖h‖ * (μ s).toReal ^ 2⁻¹

theorem MeasureTheory.integral_norm_restrict_le_norm_mul_rpow.{u_1,
    u_2}
  {α : Type u_1} {F : Type u_2}
  [MeasurableSpace α]
  [NormedAddCommGroup F]
  (μ : MeasureTheory.Measure α)
  {s : Set α} (hs : MeasurableSet s)
  (hfin : μ s ≠ ⊤)
  (h : ↥(MeasureTheory.Lp F 2 μ)) :
  ∫ (a : α) in s, ‖↑↑h a‖ ∂μ ≤
    ‖h‖ * (μ s).toReal ^ 2⁻¹

Hölder's inequality for an `L²` class on a set of finite measure: the integral of the norm
over the set is bounded by the `L²` norm times the square root of the measure of the set.  In
particular the class is integrable there, which is what makes a slice hypothesis such as the one of
`MeasureTheory.integral_L2_coeFn_ae_of_restrict` verifiable.

Because equality of the two sides is detected by testing against indicators of finite-measure sets, product integrability over all of μ\otimesν is more than the argument needs: integrability over each slice μ\otimes(ν|_s) with ν(s)<∞ already justifies the Fubini step. The slice version is what a merely locally integrable pointwise integral admits; its price is that measurability of the pointwise integral must be assumed separately, and that ν must be σ-finite for that measurability to yield the fin-strong measurability the test-set criterion consumes. The globally integrable statement is recovered as a corollary. The Hölder bound that makes a slice hypothesis checkable is proved here too: on a set of finite measure the integral of the norm of an L² class is at most its L² norm times the square root of the measure of the set, so a family whose slices are L² classes of a fixed norm is integrable on every finite-measure part.

Theorem5.1.10

uses 0used by 1✓L∃∀N

Functoriality and finite coordinate reconstruction on Bochner L^p. Mathlib's ContinuousLinearMap.compLpL applies a bounded value-space map pointwise, but its elementary functor laws were absent. A measurable set of positive finite measure gives a nonzero indicator and hence a nontrivial scalar or vector-valued L^p space. The lift is proved to preserve zero, identity, composition, subtraction, and finite sums; when scalar L^p is nontrivial it is faithful. Coordinate embeddings and projections along a finite orthonormal basis therefore give a resolution of the identity on vector-valued L^p. Consequently, if every matrix coefficient of a bounded operator on vector-valued L^p is a scalar operator on scalar L^p, the operator is the pointwise lift of one fixed bounded value-space operator. This is the finite-output substitute for introducing a completed Hilbert tensor product.

Lean code for Theorem5.1.10●14 declarations

theoremdefined in LeanRidgelet/ToMathlib/LpFunctor.lean

complete

theorem MeasureTheory.nontrivial_Lp_of_exists_measurableSet.{u_1, u_2}
  {X : Type u_1} {E : Type u_2} [MeasurableSpace X]
  [NormedAddCommGroup E] [Nontrivial E] {p : ENNReal}
  {μ : MeasureTheory.Measure X} (hp_zero : p ≠ 0) (hp_top : p ≠ ⊤)
  (s : Set X) (hs : MeasurableSet s) (hs_zero : μ s ≠ 0)
  (hs_top : μ s ≠ ⊤) : Nontrivial ↥(MeasureTheory.Lp E p μ)

theorem MeasureTheory.nontrivial_Lp_of_exists_measurableSet.{u_1,
    u_2}
  {X : Type u_1} {E : Type u_2}
  [MeasurableSpace X]
  [NormedAddCommGroup E] [Nontrivial E]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  (hp_zero : p ≠ 0) (hp_top : p ≠ ⊤)
  (s : Set X) (hs : MeasurableSet s)
  (hs_zero : μ s ≠ 0) (hs_top : μ s ≠ ⊤) :
  Nontrivial ↥(MeasureTheory.Lp E p μ)

A measurable set of positive finite measure gives a nontrivial Bochner `Lp` space for every
nonzero finite exponent.  The witness is the indicator of the set with any nonzero constant
value.

theoremdefined in LeanRidgelet/ToMathlib/LpFunctor.lean

complete

theorem ContinuousLinearMap.zero_compLpL.{u_1, u_2, u_3, u_4} {X : Type u_1}
  {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal}
  {μ : MeasureTheory.Measure X} [Fact (1 ≤ p)] :
  ContinuousLinearMap.compLpL p μ 0 = 0

theorem ContinuousLinearMap.zero_compLpL.{u_1,
    u_2, u_3, u_4}
  {X : Type u_1} {𝕜 : Type u_2}
  {E : Type u_3} {F : Type u_4}
  [MeasurableSpace X]
  [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  [Fact (1 ≤ p)] :
  ContinuousLinearMap.compLpL p μ 0 = 0

Pointwise `Lp` lifting sends the zero bounded map to zero.

theoremdefined in LeanRidgelet/ToMathlib/LpFunctor.lean

complete

theorem ContinuousLinearMap.id_compLpL.{u_1, u_2, u_3} {X : Type u_1}
  {𝕜 : Type u_2} {E : Type u_3} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {p : ENNReal} {μ : MeasureTheory.Measure X} [Fact (1 ≤ p)] :
  ContinuousLinearMap.compLpL p μ (ContinuousLinearMap.id 𝕜 E) =
    ContinuousLinearMap.id 𝕜 ↥(MeasureTheory.Lp E p μ)

theorem ContinuousLinearMap.id_compLpL.{u_1, u_2,
    u_3}
  {X : Type u_1} {𝕜 : Type u_2}
  {E : Type u_3} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  [Fact (1 ≤ p)] :
  ContinuousLinearMap.compLpL p μ
      (ContinuousLinearMap.id 𝕜 E) =
    ContinuousLinearMap.id 𝕜
      ↥(MeasureTheory.Lp E p μ)

Pointwise `Lp` lifting sends the identity bounded map to the identity.

theoremdefined in LeanRidgelet/ToMathlib/LpFunctor.lean

complete

theorem ContinuousLinearMap.comp_compLpL.{u_1, u_2, u_3, u_4, u_5}
  {X : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4}
  {G : Type u_5} [MeasurableSpace X] [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F]
  [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G]
  {p : ENNReal} {μ : MeasureTheory.Measure X} [Fact (1 ≤ p)]
  (A : F →L[𝕜] G) (B : E →L[𝕜] F) :
  ContinuousLinearMap.compLpL p μ (A ∘SL B) =
    ContinuousLinearMap.compLpL p μ A ∘SL
      ContinuousLinearMap.compLpL p μ B

theorem ContinuousLinearMap.comp_compLpL.{u_1,
    u_2, u_3, u_4, u_5}
  {X : Type u_1} {𝕜 : Type u_2}
  {E : Type u_3} {F : Type u_4}
  {G : Type u_5} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  [NormedAddCommGroup G] [NormedSpace 𝕜 G]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  [Fact (1 ≤ p)] (A : F →L[𝕜] G)
  (B : E →L[𝕜] F) :
  ContinuousLinearMap.compLpL p μ
      (A ∘SL B) =
    ContinuousLinearMap.compLpL p μ A ∘SL
      ContinuousLinearMap.compLpL p μ B

Pointwise `Lp` lifting preserves composition.

theoremdefined in LeanRidgelet/ToMathlib/LpFunctor.lean

complete

theorem ContinuousLinearMap.sub_compLpL.{u_1, u_2, u_3, u_4} {X : Type u_1}
  {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : ENNReal}
  {μ : MeasureTheory.Measure X} [Fact (1 ≤ p)] (A B : E →L[𝕜] F) :
  ContinuousLinearMap.compLpL p μ (A - B) =
    ContinuousLinearMap.compLpL p μ A -
      ContinuousLinearMap.compLpL p μ B

theorem ContinuousLinearMap.sub_compLpL.{u_1, u_2,
    u_3, u_4}
  {X : Type u_1} {𝕜 : Type u_2}
  {E : Type u_3} {F : Type u_4}
  [MeasurableSpace X]
  [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  [Fact (1 ≤ p)] (A B : E →L[𝕜] F) :
  ContinuousLinearMap.compLpL p μ
      (A - B) =
    ContinuousLinearMap.compLpL p μ A -
      ContinuousLinearMap.compLpL p μ B

Pointwise `Lp` lifting preserves subtraction.

theoremdefined in LeanRidgelet/ToMathlib/LpFunctor.lean

complete

theorem ContinuousLinearMap.finsetSum_compLpL.{u_1, u_2, u_3, u_4, u_6}
  {X : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4}
  {ι : Type u_6} [MeasurableSpace X] [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F]
  [NormedSpace 𝕜 F] {p : ENNReal} {μ : MeasureTheory.Measure X}
  [Fact (1 ≤ p)] (s : Finset ι) (A : ι → E →L[𝕜] F) :
  ContinuousLinearMap.compLpL p μ (∑ i ∈ s, A i) =
    ∑ i ∈ s, ContinuousLinearMap.compLpL p μ (A i)

theorem ContinuousLinearMap.finsetSum_compLpL.{u_1,
    u_2, u_3, u_4, u_6}
  {X : Type u_1} {𝕜 : Type u_2}
  {E : Type u_3} {F : Type u_4}
  {ι : Type u_6} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  [Fact (1 ≤ p)] (s : Finset ι)
  (A : ι → E →L[𝕜] F) :
  ContinuousLinearMap.compLpL p μ
      (∑ i ∈ s, A i) =
    ∑ i ∈ s,
      ContinuousLinearMap.compLpL p μ
        (A i)

Pointwise `Lp` lifting commutes with a finite sum of bounded maps.

theoremdefined in LeanRidgelet/ToMathlib/LpFunctor.lean

complete

theorem ContinuousLinearMap.compLpL_injective.{u_7, u_8, u_9, u_10}
  {X' : Type u_7} {K : Type u_8} {V : Type u_9} {W : Type u_10}
  [MeasurableSpace X'] [RCLike K] [NormedAddCommGroup V]
  [NormedSpace K V] [NormedAddCommGroup W] [InnerProductSpace K W]
  {q : ENNReal} {ν : MeasureTheory.Measure X'} [Fact (1 ≤ q)]
  [Nontrivial ↥(MeasureTheory.Lp K q ν)] :
  Function.Injective fun A ↦ ContinuousLinearMap.compLpL q ν A

theorem ContinuousLinearMap.compLpL_injective.{u_7,
    u_8, u_9, u_10}
  {X' : Type u_7} {K : Type u_8}
  {V : Type u_9} {W : Type u_10}
  [MeasurableSpace X'] [RCLike K]
  [NormedAddCommGroup V] [NormedSpace K V]
  [NormedAddCommGroup W]
  [InnerProductSpace K W] {q : ENNReal}
  {ν : MeasureTheory.Measure X'}
  [Fact (1 ≤ q)]
  [Nontrivial ↥(MeasureTheory.Lp K q ν)] :
  Function.Injective fun A ↦
    ContinuousLinearMap.compLpL q ν A

If scalar `Lp` is nontrivial, pointwise `Lp` lifting is faithful on bounded maps whose
codomain is an inner product space.  This is the analytic replacement for faithfulness of tensoring
with a nonzero Hilbert space in finite-output arguments.

defdefined in LeanRidgelet/ToMathlib/LpFunctor.lean

complete

def ContinuousLinearMap.lpCoordinateEmbedding.{u_7, u_8, u_9}
  {X' : Type u_7} {K : Type u_8} {V : Type u_9} [MeasurableSpace X']
  [RCLike K] [NormedAddCommGroup V] [InnerProductSpace K V]
  {q : ENNReal} {ν : MeasureTheory.Measure X'} [Fact (1 ≤ q)] (v : V) :
  ↥(MeasureTheory.Lp K q ν) →L[K] ↥(MeasureTheory.Lp V q ν)

def ContinuousLinearMap.lpCoordinateEmbedding.{u_7,
    u_8, u_9}
  {X' : Type u_7} {K : Type u_8}
  {V : Type u_9} [MeasurableSpace X']
  [RCLike K] [NormedAddCommGroup V]
  [InnerProductSpace K V] {q : ENNReal}
  {ν : MeasureTheory.Measure X'}
  [Fact (1 ≤ q)] (v : V) :
  ↥(MeasureTheory.Lp K q ν) →L[K]
    ↥(MeasureTheory.Lp V q ν)

Implementation after :=

:=
  (ContinuousLinearMap.toSpanSingleton K v).compLpL q ν

Embed scalar `Lp` into vector-valued `Lp` along a fixed value vector.

defdefined in LeanRidgelet/ToMathlib/LpFunctor.lean

complete

def ContinuousLinearMap.lpCoordinateProjection.{u_7, u_8, u_9}
  {X' : Type u_7} {K : Type u_8} {V : Type u_9} [MeasurableSpace X']
  [RCLike K] [NormedAddCommGroup V] [InnerProductSpace K V]
  {q : ENNReal} {ν : MeasureTheory.Measure X'} [Fact (1 ≤ q)] (v : V) :
  ↥(MeasureTheory.Lp V q ν) →L[K] ↥(MeasureTheory.Lp K q ν)

def ContinuousLinearMap.lpCoordinateProjection.{u_7,
    u_8, u_9}
  {X' : Type u_7} {K : Type u_8}
  {V : Type u_9} [MeasurableSpace X']
  [RCLike K] [NormedAddCommGroup V]
  [InnerProductSpace K V] {q : ENNReal}
  {ν : MeasureTheory.Measure X'}
  [Fact (1 ≤ q)] (v : V) :
  ↥(MeasureTheory.Lp V q ν) →L[K]
    ↥(MeasureTheory.Lp K q ν)

Implementation after :=

:=
  (innerSL K v).compLpL q ν

Extract the coefficient along a fixed value vector pointwise on `Lp`.

theoremdefined in LeanRidgelet/ToMathlib/LpFunctor.lean

complete

theorem ContinuousLinearMap.lpCoordinateEmbedding_apply_ae.{u_7, u_8, u_9}
  {X' : Type u_7} {K : Type u_8} {V : Type u_9} [MeasurableSpace X']
  [RCLike K] [NormedAddCommGroup V] [InnerProductSpace K V]
  {q : ENNReal} {ν : MeasureTheory.Measure X'} [Fact (1 ≤ q)] (v : V)
  (f : ↥(MeasureTheory.Lp K q ν)) :
  ↑↑((ContinuousLinearMap.lpCoordinateEmbedding v) f) =ᵐ[ν] fun x ↦
    ↑↑f x • v

theorem ContinuousLinearMap.lpCoordinateEmbedding_apply_ae.{u_7,
    u_8, u_9}
  {X' : Type u_7} {K : Type u_8}
  {V : Type u_9} [MeasurableSpace X']
  [RCLike K] [NormedAddCommGroup V]
  [InnerProductSpace K V] {q : ENNReal}
  {ν : MeasureTheory.Measure X'}
  [Fact (1 ≤ q)] (v : V)
  (f : ↥(MeasureTheory.Lp K q ν)) :
  ↑↑((ContinuousLinearMap.lpCoordinateEmbedding
            v)
          f) =ᵐ[ν]
    fun x ↦ ↑↑f x • v

theoremdefined in LeanRidgelet/ToMathlib/LpFunctor.lean

complete

theorem ContinuousLinearMap.lpCoordinateProjection_apply_ae.{u_7, u_8, u_9}
  {X' : Type u_7} {K : Type u_8} {V : Type u_9} [MeasurableSpace X']
  [RCLike K] [NormedAddCommGroup V] [InnerProductSpace K V]
  {q : ENNReal} {ν : MeasureTheory.Measure X'} [Fact (1 ≤ q)] (v : V)
  (f : ↥(MeasureTheory.Lp V q ν)) :
  ↑↑((ContinuousLinearMap.lpCoordinateProjection v) f) =ᵐ[ν] fun x ↦
    inner K v (↑↑f x)

theorem ContinuousLinearMap.lpCoordinateProjection_apply_ae.{u_7,
    u_8, u_9}
  {X' : Type u_7} {K : Type u_8}
  {V : Type u_9} [MeasurableSpace X']
  [RCLike K] [NormedAddCommGroup V]
  [InnerProductSpace K V] {q : ENNReal}
  {ν : MeasureTheory.Measure X'}
  [Fact (1 ≤ q)] (v : V)
  (f : ↥(MeasureTheory.Lp V q ν)) :
  ↑↑((ContinuousLinearMap.lpCoordinateProjection
            v)
          f) =ᵐ[ν]
    fun x ↦ inner K v (↑↑f x)

theoremdefined in LeanRidgelet/ToMathlib/LpFunctor.lean

complete

theorem ContinuousLinearMap.rankOne_compLpL_eq_coordinate_comp.{u_7, u_8, u_9}
  {X' : Type u_7} {K : Type u_8} {V : Type u_9} [MeasurableSpace X']
  [RCLike K] [NormedAddCommGroup V] [InnerProductSpace K V]
  {q : ENNReal} {ν : MeasureTheory.Measure X'} [Fact (1 ≤ q)]
  (v w : V) :
  ContinuousLinearMap.compLpL q ν
      (((InnerProductSpace.rankOne K) v) w) =
    ContinuousLinearMap.lpCoordinateEmbedding v ∘SL
      ContinuousLinearMap.lpCoordinateProjection w

theorem ContinuousLinearMap.rankOne_compLpL_eq_coordinate_comp.{u_7,
    u_8, u_9}
  {X' : Type u_7} {K : Type u_8}
  {V : Type u_9} [MeasurableSpace X']
  [RCLike K] [NormedAddCommGroup V]
  [InnerProductSpace K V] {q : ENNReal}
  {ν : MeasureTheory.Measure X'}
  [Fact (1 ≤ q)] (v w : V) :
  ContinuousLinearMap.compLpL q ν
      (((InnerProductSpace.rankOne K) v)
        w) =
    ContinuousLinearMap.lpCoordinateEmbedding
        v ∘SL
      ContinuousLinearMap.lpCoordinateProjection
        w

The pointwise rank-one operator is coordinate embedding after coordinate projection.

theoremdefined in LeanRidgelet/ToMathlib/LpFunctor.lean

complete

theorem ContinuousLinearMap.sum_lpCoordinateEmbedding_comp_projection_eq_id.{u_7,
    u_8, u_9, u_10}
  {X' : Type u_7} {K : Type u_8} {V : Type u_9} {ι' : Type u_10}
  [MeasurableSpace X'] [RCLike K] [NormedAddCommGroup V]
  [InnerProductSpace K V] {q : ENNReal} {ν : MeasureTheory.Measure X'}
  [Fact (1 ≤ q)] [Fintype ι'] (b : OrthonormalBasis ι' K V) :
  ∑ i,
      ContinuousLinearMap.lpCoordinateEmbedding (b i) ∘SL
        ContinuousLinearMap.lpCoordinateProjection (b i) =
    ContinuousLinearMap.id K ↥(MeasureTheory.Lp V q ν)

theorem ContinuousLinearMap.sum_lpCoordinateEmbedding_comp_projection_eq_id.{u_7,
    u_8, u_9, u_10}
  {X' : Type u_7} {K : Type u_8}
  {V : Type u_9} {ι' : Type u_10}
  [MeasurableSpace X'] [RCLike K]
  [NormedAddCommGroup V]
  [InnerProductSpace K V] {q : ENNReal}
  {ν : MeasureTheory.Measure X'}
  [Fact (1 ≤ q)] [Fintype ι']
  (b : OrthonormalBasis ι' K V) :
  ∑ i,
      ContinuousLinearMap.lpCoordinateEmbedding
          (b i) ∘SL
        ContinuousLinearMap.lpCoordinateProjection
          (b i) =
    ContinuousLinearMap.id K
      ↥(MeasureTheory.Lp V q ν)

A finite orthonormal basis gives a coordinate resolution of the identity on Bochner `Lp`.

theoremdefined in LeanRidgelet/ToMathlib/LpFunctor.lean

complete

theorem ContinuousLinearMap.exists_eq_compLpL_of_matrixCoefficient_scalar.{u_7,
    u_8, u_9, u_10}
  {X' : Type u_7} {K : Type u_8} {V : Type u_9} {ι' : Type u_10}
  [MeasurableSpace X'] [RCLike K] [NormedAddCommGroup V]
  [InnerProductSpace K V] {q : ENNReal} {ν : MeasureTheory.Measure X'}
  [Fact (1 ≤ q)] [Fintype ι'] (b : OrthonormalBasis ι' K V)
  (P : ↥(MeasureTheory.Lp V q ν) →L[K] ↥(MeasureTheory.Lp V q ν))
  (hP :
    ∀ (i j : ι'),
      ∃ c,
        ContinuousLinearMap.lpCoordinateProjection (b i) ∘SL
            P ∘SL ContinuousLinearMap.lpCoordinateEmbedding (b j) =
          c • ContinuousLinearMap.id K ↥(MeasureTheory.Lp K q ν)) :
  ∃ C, P = ContinuousLinearMap.compLpL q ν C

theorem ContinuousLinearMap.exists_eq_compLpL_of_matrixCoefficient_scalar.{u_7,
    u_8, u_9, u_10}
  {X' : Type u_7} {K : Type u_8}
  {V : Type u_9} {ι' : Type u_10}
  [MeasurableSpace X'] [RCLike K]
  [NormedAddCommGroup V]
  [InnerProductSpace K V] {q : ENNReal}
  {ν : MeasureTheory.Measure X'}
  [Fact (1 ≤ q)] [Fintype ι']
  (b : OrthonormalBasis ι' K V)
  (P :
    ↥(MeasureTheory.Lp V q ν) →L[K]
      ↥(MeasureTheory.Lp V q ν))
  (hP :
    ∀ (i j : ι'),
      ∃ c,
        ContinuousLinearMap.lpCoordinateProjection
              (b i) ∘SL
            P ∘SL
              ContinuousLinearMap.lpCoordinateEmbedding
                (b j) =
          c •
            ContinuousLinearMap.id K
              ↥(MeasureTheory.Lp K q ν)) :
  ∃ C,
    P = ContinuousLinearMap.compLpL q ν C

A bounded operator on vector-valued `Lp` whose matrix coefficients are scalar operators on
scalar `Lp` is the pointwise lift of one bounded value-space operator.  This finite-dimensional
reconstruction is the coordinate form of the elementary finite-factor tensor-product argument.

Theorem5.1.11

uses 0

Used by 3

Reverse dependency previews

Preview

Theorem 4.3.6

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Measurable-set projections on Bochner L^p. Multiplication by the indicator of a measurable set descends to a contractive bounded linear operator on L^p, with the expected almost-everywhere representative. It is idempotent; the whole-space and empty-set operators are respectively the identity and zero. On scalar L^2 these operators form the canonical projection family used by systems of imprimitivity: the integral formula for the L^2 inner product proves that every indicator operator is self-adjoint, so idempotence makes it an orthogonal star projection. If the star projection onto a closed subspace commutes with an indicator operator, that indicator preserves the subspace.

Lean code for Theorem5.1.11●12 declarations

theoremdefined in LeanRidgelet/ToMathlib/LpIndicator.lean

complete

theorem MeasureTheory.indicatorMemLp.{u_1, u_2} {X : Type u_1} {E : Type u_2}
  [MeasurableSpace X] [NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure X} (s : Set X) (hs : MeasurableSet s)
  (f : ↥(MeasureTheory.Lp E p μ)) :
  MeasureTheory.MemLp (s.indicator fun x ↦ ↑↑f x) p μ

theorem MeasureTheory.indicatorMemLp.{u_1, u_2}
  {X : Type u_1} {E : Type u_2}
  [MeasurableSpace X]
  [NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  (s : Set X) (hs : MeasurableSet s)
  (f : ↥(MeasureTheory.Lp E p μ)) :
  MeasureTheory.MemLp
    (s.indicator fun x ↦ ↑↑f x) p μ

The `MemLp` witness for restricting an `Lp` class to a measurable set.

defdefined in LeanRidgelet/ToMathlib/LpIndicator.lean

complete

def MeasureTheory.indicatorLpLinearMap.{u_1, u_2, u_3} {X : Type u_1}
  {E : Type u_2} {𝕜 : Type u_3} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {p : ENNReal} {μ : MeasureTheory.Measure X} (s : Set X)
  (hs : MeasurableSet s) :
  ↥(MeasureTheory.Lp E p μ) →ₗ[𝕜] ↥(MeasureTheory.Lp E p μ)

def MeasureTheory.indicatorLpLinearMap.{u_1,
    u_2, u_3}
  {X : Type u_1} {E : Type u_2}
  {𝕜 : Type u_3} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  (s : Set X) (hs : MeasurableSet s) :
  ↥(MeasureTheory.Lp E p μ) →ₗ[𝕜]
    ↥(MeasureTheory.Lp E p μ)

Implementation after :=

:= (indicatorMemLp s hs f).toLp (s.indicator fun x ↦ f x)
  map_add' f g := by
    let hsum := (Lp.memLp (f + g)).indicator hs
    let hf := (Lp.memLp f).indicator hs
    let hg := (Lp.memLp g).indicator hs
    change hsum.toLp _ = hf.toLp _ + hg.toLp _
    rw [← MemLp.toLp_add]
    apply MemLp.toLp_congr
    filter_upwards [Lp.coeFn_add f g] with x hx
    by_cases hxs : x ∈ s
    · simp only [Set.indicator_of_mem hxs, Pi.add_apply, hx]
    · simp only [Set.indicator_of_notMem hxs, Pi.add_apply, add_zero]
  map_smul' c f := by
    let hcf := (Lp.memLp (c • f)).indicator hs
    let hf := (Lp.memLp f).indicator hs
    change hcf.toLp _ = c • hf.toLp _
    rw [← MemLp.toLp_const_smul]
    apply MemLp.toLp_congr
    filter_upwards [Lp.coeFn_smul c f] with x hx
    by_cases hxs : x ∈ s
    · simp only [Set.indicator_of_mem hxs, Pi.smul_apply, hx]
    · simp only [Set.indicator_of_notMem hxs, Pi.smul_apply, smul_zero]

The linear map on `Lp` represented by multiplication by the indicator of a measurable set.

theoremdefined in LeanRidgelet/ToMathlib/LpIndicator.lean

complete

theorem MeasureTheory.indicatorLpLinearMap_apply_ae.{u_1, u_2, u_3}
  {X : Type u_1} {E : Type u_2} {𝕜 : Type u_3} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {p : ENNReal} {μ : MeasureTheory.Measure X} (s : Set X)
  (hs : MeasurableSet s) (f : ↥(MeasureTheory.Lp E p μ)) :
  ↑↑((MeasureTheory.indicatorLpLinearMap s hs) f) =ᵐ[μ]
    s.indicator fun x ↦ ↑↑f x

theorem MeasureTheory.indicatorLpLinearMap_apply_ae.{u_1,
    u_2, u_3}
  {X : Type u_1} {E : Type u_2}
  {𝕜 : Type u_3} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  (s : Set X) (hs : MeasurableSet s)
  (f : ↥(MeasureTheory.Lp E p μ)) :
  ↑↑((MeasureTheory.indicatorLpLinearMap s
            hs)
          f) =ᵐ[μ]
    s.indicator fun x ↦ ↑↑f x

The underlying indicator linear map has the expected pointwise representative.

defdefined in LeanRidgelet/ToMathlib/LpIndicator.lean

complete

def MeasureTheory.indicatorLp.{u_1, u_2, u_3} {X : Type u_1} {E : Type u_2}
  {𝕜 : Type u_3} [MeasurableSpace X] [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : ENNReal}
  {μ : MeasureTheory.Measure X} [Fact (1 ≤ p)] (s : Set X)
  (hs : MeasurableSet s) :
  ↥(MeasureTheory.Lp E p μ) →L[𝕜] ↥(MeasureTheory.Lp E p μ)

def MeasureTheory.indicatorLp.{u_1, u_2, u_3}
  {X : Type u_1} {E : Type u_2}
  {𝕜 : Type u_3} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  [Fact (1 ≤ p)] (s : Set X)
  (hs : MeasurableSet s) :
  ↥(MeasureTheory.Lp E p μ) →L[𝕜]
    ↥(MeasureTheory.Lp E p μ)

Implementation after :=

:=
  (indicatorLpLinearMap (p := p) (μ := μ) (E := E) (𝕜 := 𝕜) s hs).mkContinuous 1 fun f ↦ by
    apply Lp.norm_le_mul_norm_of_ae_le_mul
    have hout := indicatorLpLinearMap_apply_ae
      (p := p) (μ := μ) (E := E) (𝕜 := 𝕜) s hs f
    filter_upwards [hout] with x hx
    rw [hx]
    by_cases hxs : x ∈ s
    · simp only [Set.indicator_of_mem hxs, one_mul]
      exact le_rfl
    · simp only [Set.indicator_of_notMem hxs, norm_zero, one_mul, norm_nonneg]

Multiplication by a measurable indicator as a contractive bounded linear operator on `Lp`.

theoremdefined in LeanRidgelet/ToMathlib/LpIndicator.lean

complete

theorem MeasureTheory.indicatorLp_apply_ae.{u_1, u_2, u_3} {X : Type u_1}
  {E : Type u_2} {𝕜 : Type u_3} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {p : ENNReal} {μ : MeasureTheory.Measure X} [Fact (1 ≤ p)] (s : Set X)
  (hs : MeasurableSet s) (f : ↥(MeasureTheory.Lp E p μ)) :
  ↑↑((MeasureTheory.indicatorLp s hs) f) =ᵐ[μ] s.indicator fun x ↦ ↑↑f x

theorem MeasureTheory.indicatorLp_apply_ae.{u_1,
    u_2, u_3}
  {X : Type u_1} {E : Type u_2}
  {𝕜 : Type u_3} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  [Fact (1 ≤ p)] (s : Set X)
  (hs : MeasurableSet s)
  (f : ↥(MeasureTheory.Lp E p μ)) :
  ↑↑((MeasureTheory.indicatorLp s hs)
          f) =ᵐ[μ]
    s.indicator fun x ↦ ↑↑f x

The indicator operator has the expected pointwise representative.

theoremdefined in LeanRidgelet/ToMathlib/LpIndicator.lean

complete

theorem MeasureTheory.indicatorLp_comp_self.{u_1, u_2, u_3} {X : Type u_1}
  {E : Type u_2} {𝕜 : Type u_3} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {p : ENNReal} {μ : MeasureTheory.Measure X} [Fact (1 ≤ p)] (s : Set X)
  (hs : MeasurableSet s) :
  MeasureTheory.indicatorLp s hs ∘SL MeasureTheory.indicatorLp s hs =
    MeasureTheory.indicatorLp s hs

theorem MeasureTheory.indicatorLp_comp_self.{u_1,
    u_2, u_3}
  {X : Type u_1} {E : Type u_2}
  {𝕜 : Type u_3} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  [Fact (1 ≤ p)] (s : Set X)
  (hs : MeasurableSet s) :
  MeasureTheory.indicatorLp s hs ∘SL
      MeasureTheory.indicatorLp s hs =
    MeasureTheory.indicatorLp s hs

Indicator multiplication is idempotent.

theoremdefined in LeanRidgelet/ToMathlib/LpIndicator.lean

complete

theorem MeasureTheory.indicatorLp_univ.{u_1, u_2, u_3} {X : Type u_1}
  {E : Type u_2} {𝕜 : Type u_3} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {p : ENNReal} {μ : MeasureTheory.Measure X} [Fact (1 ≤ p)] :
  MeasureTheory.indicatorLp Set.univ ⋯ =
    ContinuousLinearMap.id 𝕜 ↥(MeasureTheory.Lp E p μ)

theorem MeasureTheory.indicatorLp_univ.{u_1, u_2,
    u_3}
  {X : Type u_1} {E : Type u_2}
  {𝕜 : Type u_3} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  [Fact (1 ≤ p)] :
  MeasureTheory.indicatorLp Set.univ ⋯ =
    ContinuousLinearMap.id 𝕜
      ↥(MeasureTheory.Lp E p μ)

The indicator of the whole space is the identity operator on `Lp`.

theoremdefined in LeanRidgelet/ToMathlib/LpIndicator.lean

complete

theorem MeasureTheory.indicatorLp_empty.{u_1, u_2, u_3} {X : Type u_1}
  {E : Type u_2} {𝕜 : Type u_3} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {p : ENNReal} {μ : MeasureTheory.Measure X} [Fact (1 ≤ p)] :
  MeasureTheory.indicatorLp ∅ ⋯ = 0

theorem MeasureTheory.indicatorLp_empty.{u_1, u_2,
    u_3}
  {X : Type u_1} {E : Type u_2}
  {𝕜 : Type u_3} [MeasurableSpace X]
  [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {p : ENNReal}
  {μ : MeasureTheory.Measure X}
  [Fact (1 ≤ p)] :
  MeasureTheory.indicatorLp ∅ ⋯ = 0

The indicator of the empty set is the zero operator on `Lp`.

theoremdefined in LeanRidgelet/ToMathlib/LpIndicator.lean

complete

theorem MeasureTheory.indicatorLp_isSelfAdjoint.{u_1} {X : Type u_1}
  [MeasurableSpace X] {μ : MeasureTheory.Measure X} (s : Set X)
  (hs : MeasurableSet s) :
  IsSelfAdjoint (MeasureTheory.indicatorLp s hs)

theorem MeasureTheory.indicatorLp_isSelfAdjoint.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  (s : Set X) (hs : MeasurableSet s) :
  IsSelfAdjoint
    (MeasureTheory.indicatorLp s hs)

On scalar complex `L²`, multiplication by a measurable indicator is self-adjoint.

theoremdefined in LeanRidgelet/ToMathlib/LpIndicator.lean

complete

theorem MeasureTheory.indicatorLp_isStarProjection.{u_1} {X : Type u_1}
  [MeasurableSpace X] {μ : MeasureTheory.Measure X} (s : Set X)
  (hs : MeasurableSet s) :
  IsStarProjection (MeasureTheory.indicatorLp s hs)

theorem MeasureTheory.indicatorLp_isStarProjection.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  (s : Set X) (hs : MeasurableSet s) :
  IsStarProjection
    (MeasureTheory.indicatorLp s hs)

On scalar complex `L²`, multiplication by a measurable indicator is an orthogonal
projection.

theoremdefined in LeanRidgelet/ToMathlib/LpIndicator.lean

complete

theorem MeasureTheory.indicatorLp_mem_of_starProjection_commute.{u_1}
  {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  (K : ClosedSubmodule ℂ ↥(MeasureTheory.Lp ℂ 2 μ)) (s : Set X)
  (hs : MeasurableSet s)
  (hcommute :
    (↑K).starProjection ∘SL MeasureTheory.indicatorLp s hs =
      MeasureTheory.indicatorLp s hs ∘SL (↑K).starProjection)
  {f : ↥(MeasureTheory.Lp ℂ 2 μ)} (hf : f ∈ K) :
  (MeasureTheory.indicatorLp s hs) f ∈ K

theorem MeasureTheory.indicatorLp_mem_of_starProjection_commute.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  (K :
    ClosedSubmodule ℂ
      ↥(MeasureTheory.Lp ℂ 2 μ))
  (s : Set X) (hs : MeasurableSet s)
  (hcommute :
    (↑K).starProjection ∘SL
        MeasureTheory.indicatorLp s hs =
      MeasureTheory.indicatorLp s hs ∘SL
        (↑K).starProjection)
  {f : ↥(MeasureTheory.Lp ℂ 2 μ)}
  (hf : f ∈ K) :
  (MeasureTheory.indicatorLp s hs) f ∈ K

If the orthogonal projection onto a closed subspace commutes with a measurable-set
projection, then that closed subspace is stable under the corresponding indicator
multiplication.

theoremdefined in LeanRidgelet/ToMathlib/LpIndicator.lean

complete

theorem MeasureTheory.ae_eq_zero_of_mem_orthogonal_of_indicatorLp_mem.{u_1}
  {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  {K : Submodule ℂ ↥(MeasureTheory.Lp ℂ 2 μ)}
  {f v : ↥(MeasureTheory.Lp ℂ 2 μ)}
  (hf :
    ∀ (s : Set X) (hs : MeasurableSet s),
      (MeasureTheory.indicatorLp s hs) f ∈ K)
  (hv : v ∈ Kᗮ) : ∀ᵐ (x : X) ∂μ, ↑↑f x ≠ 0 → ↑↑v x = 0

theorem MeasureTheory.ae_eq_zero_of_mem_orthogonal_of_indicatorLp_mem.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  {K :
    Submodule ℂ ↥(MeasureTheory.Lp ℂ 2 μ)}
  {f v : ↥(MeasureTheory.Lp ℂ 2 μ)}
  (hf :
    ∀ (s : Set X) (hs : MeasurableSet s),
      (MeasureTheory.indicatorLp s hs) f ∈
        K)
  (hv : v ∈ Kᗮ) :
  ∀ᵐ (x : X) ∂μ, ↑↑f x ≠ 0 → ↑↑v x = 0

If every measurable indicator restriction of `f` belongs to a submodule of scalar `L²`, then
every vector orthogonal to that submodule vanishes almost everywhere on the set where `f` does not
vanish.

Testing orthogonality against the indicator restrictions of `f` says exactly that the integrable
pointwise inner product `⟪f, v⟫` has vanishing integral over every measurable set, hence vanishes
almost everywhere.  This is the elementary mechanism behind the fact that a closed subspace stable
under all multiplication projections is the set of vectors supported in a fixed measurable set.

If a submodule contains every indicator restriction of a fixed vector f, then testing orthogonality against those restrictions says that the integrable pointwise inner product \langle f,v\rangle has vanishing integral over every measurable set. Hence a vector orthogonal to the submodule vanishes almost everywhere on the set where f does not vanish.

Theorem5.1.12

uses 1used by 1✓L∃∀N

Compactly supported scalar multipliers on L^2. A compactly supported continuous scalar function is uniformly approximated by measurable simple functions. Its simple multipliers are finite linear combinations of indicator projections, so every closed subspace stable under all measurable indicators is stable under compactly supported continuous multiplication. Combining this with Mathlib's regular-measure approximation theorem and an Urysohn cutoff shows that a continuous L^2 representative can be approximated by compactly supported continuous representatives in the same closed subspace.

Lean code for Theorem5.1.12●10 declarations

theoremdefined in LeanRidgelet/ToMathlib/LpCompactlySupportedMultiplier.lean

complete

theorem HasCompactSupport.exists_simpleFunc_approx.{u_1, u_2} {X : Type u_1}
  {F : Type u_2} [TopologicalSpace X] [R1Space X] [MeasurableSpace X]
  [OpensMeasurableSpace X] [PseudoMetricSpace F] [Zero F] {f : X → F}
  (hf : Continuous f) (h'f : HasCompactSupport f) {ε : ℝ} (hε : 0 < ε) :
  ∃ g, ∀ (x : X), dist (f x) (g x) < ε

theorem HasCompactSupport.exists_simpleFunc_approx.{u_1,
    u_2}
  {X : Type u_1} {F : Type u_2}
  [TopologicalSpace X] [R1Space X]
  [MeasurableSpace X]
  [OpensMeasurableSpace X]
  [PseudoMetricSpace F] [Zero F]
  {f : X → F} (hf : Continuous f)
  (h'f : HasCompactSupport f) {ε : ℝ}
  (hε : 0 < ε) :
  ∃ g, ∀ (x : X), dist (f x) (g x) < ε

A compactly supported continuous function on one measurable space can be uniformly
approximated by measurable simple functions.  Mathlib provides the product-space version; the
one-space statement follows by adjoining a `PUnit` factor.

defdefined in LeanRidgelet/ToMathlib/LpCompactlySupportedMultiplier.lean

complete

def MeasureTheory.simpleFuncMultiplierLp.{u_1} {X : Type u_1}
  [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  (s : MeasureTheory.SimpleFunc X ℂ) (f : ↥(MeasureTheory.Lp ℂ 2 μ)) :
  ↥(MeasureTheory.Lp ℂ 2 μ)

def MeasureTheory.simpleFuncMultiplierLp.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  (s : MeasureTheory.SimpleFunc X ℂ)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ)) :
  ↥(MeasureTheory.Lp ℂ 2 μ)

Implementation after :=

:=
  ∑ c ∈ s.range, c • indicatorLp (p := (2 : ℝ≥0∞)) (μ := μ) (E := ℂ) (𝕜 := ℂ)
    (⇑s ⁻¹' {c}) (s.measurableSet_fiber c) f

The `Lp` multiplier associated with a measurable complex simple function, expressed as a
finite linear combination of measurable indicator projections.

theoremdefined in LeanRidgelet/ToMathlib/LpCompactlySupportedMultiplier.lean

complete

theorem MeasureTheory.simpleFuncMultiplierLp_apply_ae.{u_1} {X : Type u_1}
  [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  (s : MeasureTheory.SimpleFunc X ℂ) (f : ↥(MeasureTheory.Lp ℂ 2 μ)) :
  ↑↑(MeasureTheory.simpleFuncMultiplierLp s f) =ᵐ[μ] fun x ↦ s x * ↑↑f x

theorem MeasureTheory.simpleFuncMultiplierLp_apply_ae.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  (s : MeasureTheory.SimpleFunc X ℂ)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ)) :
  ↑↑(MeasureTheory.simpleFuncMultiplierLp
          s f) =ᵐ[μ]
    fun x ↦ s x * ↑↑f x

A simple-function multiplier has its expected pointwise representative.

theoremdefined in LeanRidgelet/ToMathlib/LpCompactlySupportedMultiplier.lean

complete

theorem MeasureTheory.simpleFuncMultiplierLp_mem_of_indicatorLp_mem.{u_1}
  {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  (K : ClosedSubmodule ℂ ↥(MeasureTheory.Lp ℂ 2 μ))
  (s : MeasureTheory.SimpleFunc X ℂ) {f : ↥(MeasureTheory.Lp ℂ 2 μ)}
  (hindicator :
    ∀ (t : Set X) (ht : MeasurableSet t),
      (MeasureTheory.indicatorLp t ht) f ∈ K) :
  MeasureTheory.simpleFuncMultiplierLp s f ∈ K

theorem MeasureTheory.simpleFuncMultiplierLp_mem_of_indicatorLp_mem.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  (K :
    ClosedSubmodule ℂ
      ↥(MeasureTheory.Lp ℂ 2 μ))
  (s : MeasureTheory.SimpleFunc X ℂ)
  {f : ↥(MeasureTheory.Lp ℂ 2 μ)}
  (hindicator :
    ∀ (t : Set X) (ht : MeasurableSet t),
      (MeasureTheory.indicatorLp t ht) f ∈
        K) :
  MeasureTheory.simpleFuncMultiplierLp s
      f ∈
    K

Stability under all measurable indicator projections implies stability under a measurable
simple scalar multiplier.

theoremdefined in LeanRidgelet/ToMathlib/LpCompactlySupportedMultiplier.lean

complete

theorem MeasureTheory.compactlySupportedContinuous_memLp.{u_1} {X : Type u_1}
  [MeasurableSpace X] {μ : MeasureTheory.Measure X} [TopologicalSpace X]
  [BorelSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  (f : CompactlySupportedContinuousMap X ℂ) :
  MeasureTheory.MemLp (⇑f) 2 μ

theorem MeasureTheory.compactlySupportedContinuous_memLp.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  [TopologicalSpace X] [BorelSpace X]
  [MeasureTheory.IsFiniteMeasureOnCompacts
      μ]
  (f :
    CompactlySupportedContinuousMap X ℂ) :
  MeasureTheory.MemLp (⇑f) 2 μ

A compactly supported continuous scalar function belongs to every finite-exponent `Lp` space
for a measure finite on compact sets.

defdefined in LeanRidgelet/ToMathlib/LpCompactlySupportedMultiplier.lean

complete

def MeasureTheory.compactlySupportedContinuousToLp.{u_1} {X : Type u_1}
  [MeasurableSpace X] {μ : MeasureTheory.Measure X} [TopologicalSpace X]
  [BorelSpace X] [MeasureTheory.IsFiniteMeasureOnCompacts μ] :
  CompactlySupportedContinuousMap X ℂ →ₗ[ℂ] ↥(MeasureTheory.Lp ℂ 2 μ)

def MeasureTheory.compactlySupportedContinuousToLp.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  [TopologicalSpace X] [BorelSpace X]
  [MeasureTheory.IsFiniteMeasureOnCompacts
      μ] :
  CompactlySupportedContinuousMap X
      ℂ →ₗ[ℂ]
    ↥(MeasureTheory.Lp ℂ 2 μ)

Implementation after :=

:= (compactlySupportedContinuous_memLp f).toLp f
  map_add' f g := by
    rw [← MemLp.toLp_add]
    apply MemLp.toLp_congr
    exact Filter.Eventually.of_forall fun x ↦ by simp
  map_smul' c f := by
    rw [← MemLp.toLp_const_smul]
    apply MemLp.toLp_congr
    exact Filter.Eventually.of_forall fun x ↦ by simp

The linear map sending a compactly supported continuous scalar function to its `L²` class.

defdefined in LeanRidgelet/ToMathlib/LpCompactlySupportedMultiplier.lean

complete

def MeasureTheory.compactlySupportedContinuousMultiplierLp.{u_1}
  {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [TopologicalSpace X] [BorelSpace X]
  (φ : CompactlySupportedContinuousMap X ℂ)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ)) : ↥(MeasureTheory.Lp ℂ 2 μ)

def MeasureTheory.compactlySupportedContinuousMultiplierLp.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  [TopologicalSpace X] [BorelSpace X]
  (φ :
    CompactlySupportedContinuousMap X ℂ)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ)) :
  ↥(MeasureTheory.Lp ℂ 2 μ)

Implementation after :=

:= by
  let C : ℝ := ‖φ.toBoundedContinuousFunction‖
  have hmem : MemLp (fun x ↦ φ x * f x) 2 μ := by
    apply MemLp.of_le_mul (c := C) (Lp.memLp f)
      (φ.continuous.aestronglyMeasurable.mul (Lp.aestronglyMeasurable f))
    filter_upwards with x
    change ‖φ x * f x‖ ≤ C * ‖f x‖
    rw [norm_mul]
    exact mul_le_mul_of_nonneg_right
      (φ.toBoundedContinuousFunction.norm_coe_le_norm x) (norm_nonneg _)
  exact hmem.toLp fun x ↦ φ x * f x

Multiplication of an `Lp` class by a compactly supported continuous scalar function.

theoremdefined in LeanRidgelet/ToMathlib/LpCompactlySupportedMultiplier.lean

complete

theorem MeasureTheory.compactlySupportedContinuousMultiplierLp_apply_ae.{u_1}
  {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [TopologicalSpace X] [BorelSpace X]
  (φ : CompactlySupportedContinuousMap X ℂ)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ)) :
  ↑↑(MeasureTheory.compactlySupportedContinuousMultiplierLp φ f) =ᵐ[μ]
    fun x ↦ φ x * ↑↑f x

theorem MeasureTheory.compactlySupportedContinuousMultiplierLp_apply_ae.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  [TopologicalSpace X] [BorelSpace X]
  (φ :
    CompactlySupportedContinuousMap X ℂ)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ)) :
  ↑↑(MeasureTheory.compactlySupportedContinuousMultiplierLp
          φ f) =ᵐ[μ]
    fun x ↦ φ x * ↑↑f x

The compactly supported continuous multiplier has its expected pointwise representative.

theoremdefined in LeanRidgelet/ToMathlib/LpCompactlySupportedMultiplier.lean

complete

theorem MeasureTheory.compactlySupportedContinuousMultiplierLp_mem_of_indicatorLp_mem.{u_1}
  {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [TopologicalSpace X] [R1Space X] [BorelSpace X]
  (K : ClosedSubmodule ℂ ↥(MeasureTheory.Lp ℂ 2 μ))
  (φ : CompactlySupportedContinuousMap X ℂ)
  {f : ↥(MeasureTheory.Lp ℂ 2 μ)}
  (hindicator :
    ∀ (t : Set X) (ht : MeasurableSet t),
      (MeasureTheory.indicatorLp t ht) f ∈ K) :
  MeasureTheory.compactlySupportedContinuousMultiplierLp φ f ∈ K

theorem MeasureTheory.compactlySupportedContinuousMultiplierLp_mem_of_indicatorLp_mem.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  [TopologicalSpace X] [R1Space X]
  [BorelSpace X]
  (K :
    ClosedSubmodule ℂ
      ↥(MeasureTheory.Lp ℂ 2 μ))
  (φ :
    CompactlySupportedContinuousMap X ℂ)
  {f : ↥(MeasureTheory.Lp ℂ 2 μ)}
  (hindicator :
    ∀ (t : Set X) (ht : MeasurableSet t),
      (MeasureTheory.indicatorLp t ht) f ∈
        K) :
  MeasureTheory.compactlySupportedContinuousMultiplierLp
      φ f ∈
    K

A closed subspace stable under every measurable indicator projection is stable under every
compactly supported continuous scalar multiplier.

theoremdefined in LeanRidgelet/ToMathlib/LpCompactlySupportedMultiplier.lean

complete

theorem MeasureTheory.exists_compactlySupportedContinuousToLp_mem_dist_lt.{u_1}
  {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [TopologicalSpace X] [R1Space X] [BorelSpace X]
  [LocallyCompactSpace X] [NormalSpace X] [μ.Regular]
  (K : ClosedSubmodule ℂ ↥(MeasureTheory.Lp ℂ 2 μ)) {g : X → ℂ}
  (hgcontinuous : Continuous g) (hgmem : MeasureTheory.MemLp g 2 μ)
  (hindicator :
    ∀ (t : Set X) (ht : MeasurableSet t),
      (MeasureTheory.indicatorLp t ht)
          (MeasureTheory.MemLp.toLp g hgmem) ∈
        K)
  {ε : ℝ} (hε : 0 < ε) :
  ∃ r,
    MeasureTheory.compactlySupportedContinuousToLp r ∈ K ∧
      dist (MeasureTheory.compactlySupportedContinuousToLp r)
          (MeasureTheory.MemLp.toLp g hgmem) <
        ε

theorem MeasureTheory.exists_compactlySupportedContinuousToLp_mem_dist_lt.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  [TopologicalSpace X] [R1Space X]
  [BorelSpace X] [LocallyCompactSpace X]
  [NormalSpace X] [μ.Regular]
  (K :
    ClosedSubmodule ℂ
      ↥(MeasureTheory.Lp ℂ 2 μ))
  {g : X → ℂ}
  (hgcontinuous : Continuous g)
  (hgmem : MeasureTheory.MemLp g 2 μ)
  (hindicator :
    ∀ (t : Set X) (ht : MeasurableSet t),
      (MeasureTheory.indicatorLp t ht)
          (MeasureTheory.MemLp.toLp g
            hgmem) ∈
        K)
  {ε : ℝ} (hε : 0 < ε) :
  ∃ r,
    MeasureTheory.compactlySupportedContinuousToLp
          r ∈
        K ∧
      dist
          (MeasureTheory.compactlySupportedContinuousToLp
            r)
          (MeasureTheory.MemLp.toLp g
            hgmem) <
        ε

If a continuous representative belongs to a closed subspace stable under measurable
indicators, then it can be approximated by compactly supported continuous representatives in the
same subspace.

Theorem5.1.13

uses 1used by 1✓L∃∀N

Fourier characters generate measurable multipliers on L^2. A measurable embedding into a finite-dimensional real inner-product space pulls Mathlib's normalized Fourier characters back to unitary multiplication operators. A bounded operator commuting with all these character multipliers also commutes with every finite complex character sum. Finite character sums are dense in L^2 of every finite measure: an orthogonal vector is first regarded as an integrable density; the positive and negative parts of its real and imaginary components define finite measures, and Mathlib's characteristic-function uniqueness theorem makes those measures equal. The weighted- measure calculation then gives simultaneous approximation of two L^2 vectors, and a strong-limit argument yields commutation with every indicator projection. No general projection-valued-measure API is introduced.

Lean code for Theorem5.1.13●12 declarations

theoremdefined in LeanRidgelet/ToMathlib/FourierCharacterMultiplier.lean

complete

theorem MeasureTheory.eLpNorm_mul_eq_eLpNorm_withDensity_enorm_sq.{u_1}
  {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  (u f : X → ℂ) (hu : MeasureTheory.AEStronglyMeasurable u μ)
  (hf : MeasureTheory.AEStronglyMeasurable f μ) :
  MeasureTheory.eLpNorm (fun x ↦ u x * f x) 2 μ =
    MeasureTheory.eLpNorm u 2 (μ.withDensity fun x ↦ ‖f x‖ₑ ^ 2)

theorem MeasureTheory.eLpNorm_mul_eq_eLpNorm_withDensity_enorm_sq.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  (u f : X → ℂ)
  (hu :
    MeasureTheory.AEStronglyMeasurable u
      μ)
  (hf :
    MeasureTheory.AEStronglyMeasurable f
      μ) :
  MeasureTheory.eLpNorm
      (fun x ↦ u x * f x) 2 μ =
    MeasureTheory.eLpNorm u 2
      (μ.withDensity fun x ↦ ‖f x‖ₑ ^ 2)

The `L²(μ)` seminorm of a pointwise product is the seminorm of the first factor for the
measure weighted by the squared norm of the second factor.

defdefined in LeanRidgelet/ToMathlib/FourierCharacterMultiplier.lean

complete

def MeasureTheory.fourierCharacterMultiplierPhase.{u_1, u_2} {X : Type u_1}
  {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  (j : X → V) (b : V) (x : X) : ℂ

def MeasureTheory.fourierCharacterMultiplierPhase.{u_1,
    u_2}
  {X : Type u_1} {V : Type u_2}
  [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] (j : X → V)
  (b : V) (x : X) : ℂ

Implementation after :=

:=
  Real.fourierChar (-⟪b, j x⟫_ℝ)

The Fourier character on `V`, pulled back along a map `j : X → V`.  The sign and the
`2π` normalization agree with Mathlib's Fourier transform.

theoremdefined in LeanRidgelet/ToMathlib/FourierCharacterMultiplier.lean

complete

theorem MeasureTheory.fourierCharacterMultiplierPhase_aestronglyMeasurable.{u_1,
    u_2}
  {X : Type u_1} {V : Type u_2} [MeasurableSpace X]
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure X}
  (j : X → V) (hj : Measurable j) (b : V) :
  MeasureTheory.AEStronglyMeasurable
    (MeasureTheory.fourierCharacterMultiplierPhase j b) μ

theorem MeasureTheory.fourierCharacterMultiplierPhase_aestronglyMeasurable.{u_1,
    u_2}
  {X : Type u_1} {V : Type u_2}
  [MeasurableSpace X]
  [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  {μ : MeasureTheory.Measure X}
  (j : X → V) (hj : Measurable j)
  (b : V) :
  MeasureTheory.AEStronglyMeasurable
    (MeasureTheory.fourierCharacterMultiplierPhase
      j b)
    μ

A measurable pullback of a Fourier character is strongly measurable.

theoremdefined in LeanRidgelet/ToMathlib/FourierCharacterMultiplier.lean

complete

theorem MeasureTheory.fourierCharacterMultiplierPhase_norm_one.{u_1, u_2}
  {X : Type u_1} {V : Type u_2} [MeasurableSpace X]
  [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  {μ : MeasureTheory.Measure X} (j : X → V) (b : V) :
  ∀ᵐ (x : X) ∂μ,
    ‖MeasureTheory.fourierCharacterMultiplierPhase j b x‖ = 1

theorem MeasureTheory.fourierCharacterMultiplierPhase_norm_one.{u_1,
    u_2}
  {X : Type u_1} {V : Type u_2}
  [MeasurableSpace X]
  [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  {μ : MeasureTheory.Measure X}
  (j : X → V) (b : V) :
  ∀ᵐ (x : X) ∂μ,
    ‖MeasureTheory.fourierCharacterMultiplierPhase
          j b x‖ =
      1

Pulled-back Fourier characters are pointwise unimodular.

defdefined in LeanRidgelet/ToMathlib/FourierCharacterMultiplier.lean

complete

def MeasureTheory.fourierCharacterLpMultiplier.{u_1, u_2} {X : Type u_1}
  {V : Type u_2} [MeasurableSpace X] [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V]
  [BorelSpace V] {μ : MeasureTheory.Measure X} (j : X → V)
  (hj : Measurable j) (b : V) :
  ↥(MeasureTheory.Lp ℂ 2 μ) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ 2 μ)

def MeasureTheory.fourierCharacterLpMultiplier.{u_1,
    u_2}
  {X : Type u_1} {V : Type u_2}
  [MeasurableSpace X]
  [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  {μ : MeasureTheory.Measure X}
  (j : X → V) (hj : Measurable j)
  (b : V) :
  ↥(MeasureTheory.Lp ℂ 2 μ) ≃ₗᵢ[ℂ]
    ↥(MeasureTheory.Lp ℂ 2 μ)

Implementation after :=

:=
  unimodularMultiplierLinearIsometryEquiv (fourierCharacterMultiplierPhase j b)
    (fourierCharacterMultiplierPhase_aestronglyMeasurable (μ := μ) j hj b)
    (fourierCharacterMultiplierPhase_norm_one (μ := μ) j b)

Multiplication by a pulled-back Fourier character, bundled as a unitary `L²` operator.

theoremdefined in LeanRidgelet/ToMathlib/FourierCharacterMultiplier.lean

complete

theorem MeasureTheory.fourierCharacterLpMultiplier_apply_ae.{u_1, u_2}
  {X : Type u_1} {V : Type u_2} [MeasurableSpace X]
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure X}
  (j : X → V) (hj : Measurable j) (b : V)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ)) :
  ↑↑((MeasureTheory.fourierCharacterLpMultiplier j hj b) f) =ᵐ[μ]
    fun x ↦ MeasureTheory.fourierCharacterMultiplierPhase j b x * ↑↑f x

theorem MeasureTheory.fourierCharacterLpMultiplier_apply_ae.{u_1,
    u_2}
  {X : Type u_1} {V : Type u_2}
  [MeasurableSpace X]
  [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  {μ : MeasureTheory.Measure X}
  (j : X → V) (hj : Measurable j) (b : V)
  (f : ↥(MeasureTheory.Lp ℂ 2 μ)) :
  ↑↑((MeasureTheory.fourierCharacterLpMultiplier
            j hj b)
          f) =ᵐ[μ]
    fun x ↦
    MeasureTheory.fourierCharacterMultiplierPhase
        j b x *
      ↑↑f x

The bundled Fourier-character multiplier has its defining pointwise representative.

theoremdefined in LeanRidgelet/ToMathlib/FourierCharacterMultiplier.lean

complete

theorem MeasureTheory.integrable_real_eq_zero_of_integral_fourierChar_inner.{u_2}
  {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V]
  {ν : MeasureTheory.Measure V} [MeasureTheory.IsFiniteMeasure ν]
  (r : V → ℝ) (hrm : Measurable r) (hr : MeasureTheory.Integrable r ν)
  (hzero :
    ∀ (b : V),
      ∫ (x : V), ↑(Real.fourierChar (inner ℝ x b)) * ↑(r x) ∂ν = 0) :
  r =ᵐ[ν] 0

theorem MeasureTheory.integrable_real_eq_zero_of_integral_fourierChar_inner.{u_2}
  {V : Type u_2} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  {ν : MeasureTheory.Measure V}
  [MeasureTheory.IsFiniteMeasure ν]
  (r : V → ℝ) (hrm : Measurable r)
  (hr : MeasureTheory.Integrable r ν)
  (hzero :
    ∀ (b : V),
      ∫ (x : V),
          ↑(Real.fourierChar
                (inner ℝ x b)) *
            ↑(r x) ∂ν =
        0) :
  r =ᵐ[ν] 0

A real integrable density on a finite-dimensional real inner-product space is almost
everywhere zero if all of its Fourier-character integrals vanish.

theoremdefined in LeanRidgelet/ToMathlib/FourierCharacterMultiplier.lean

complete

theorem MeasureTheory.integrable_complex_eq_zero_of_integral_fourierChar_inner.{u_2}
  {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V]
  {ν : MeasureTheory.Measure V} [MeasureTheory.IsFiniteMeasure ν]
  (f : V → ℂ) (hfm : Measurable f) (hf : MeasureTheory.Integrable f ν)
  (hzero :
    ∀ (b : V),
      ∫ (x : V), ↑(Real.fourierChar (inner ℝ x b)) * f x ∂ν = 0) :
  f =ᵐ[ν] 0

theorem MeasureTheory.integrable_complex_eq_zero_of_integral_fourierChar_inner.{u_2}
  {V : Type u_2} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  {ν : MeasureTheory.Measure V}
  [MeasureTheory.IsFiniteMeasure ν]
  (f : V → ℂ) (hfm : Measurable f)
  (hf : MeasureTheory.Integrable f ν)
  (hzero :
    ∀ (b : V),
      ∫ (x : V),
          ↑(Real.fourierChar
                (inner ℝ x b)) *
            f x ∂ν =
        0) :
  f =ᵐ[ν] 0

A complex integrable density on a finite-dimensional real inner-product space is almost
everywhere zero if all of its Fourier-character integrals vanish.

theoremdefined in LeanRidgelet/ToMathlib/FourierCharacterMultiplier.lean

complete

theorem MeasureTheory.exists_fourierCharacter_finset_approx_indicator_eLpNorm.{u_2}
  {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V]
  {ν : MeasureTheory.Measure V} [MeasureTheory.IsFiniteMeasure ν]
  (s : Set V) (hs : MeasurableSet s) {epsilon : ENNReal}
  (hepsilon : epsilon ≠ 0) :
  ∃ t c,
    MeasureTheory.eLpNorm
        (fun x ↦
          ∑ b ∈ t,
              c b *
                MeasureTheory.fourierCharacterMultiplierPhase id b x -
            s.indicator (fun x ↦ 1) x)
        2 ν <
      epsilon

theorem MeasureTheory.exists_fourierCharacter_finset_approx_indicator_eLpNorm.{u_2}
  {V : Type u_2} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  {ν : MeasureTheory.Measure V}
  [MeasureTheory.IsFiniteMeasure ν]
  (s : Set V) (hs : MeasurableSet s)
  {epsilon : ENNReal}
  (hepsilon : epsilon ≠ 0) :
  ∃ t c,
    MeasureTheory.eLpNorm
        (fun x ↦
          ∑ b ∈ t,
              c b *
                MeasureTheory.fourierCharacterMultiplierPhase
                  id b x -
            s.indicator (fun x ↦ 1) x)
        2 ν <
      epsilon

On a finite measure over `V`, finite complex linear combinations of Fourier characters
approximate every measurable indicator in `L²` seminorm.

This is the analytic density input to the multiplier form of Folland's Theorem 4.44.  The proof
identifies the orthogonal complement of the character span with integrable densities whose
characteristic function vanishes, applies `MeasureTheory.ext_of_integral_char_eq` to the positive
and negative parts of the real and imaginary components, and then uses
`Submodule.topologicalClosure_eq_top_iff`.

theoremdefined in LeanRidgelet/ToMathlib/FourierCharacterMultiplier.lean

complete

theorem MeasureTheory.exists_finsetSum_fourierCharacterLpMultiplier_approx_indicatorLp.{u_1,
    u_2}
  {X : Type u_1} {V : Type u_2} [MeasurableSpace X]
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure X}
  (j : X → V) (hj : MeasurableEmbedding j)
  (f g : ↥(MeasureTheory.Lp ℂ 2 μ)) (s : Set X) (hs : MeasurableSet s)
  {epsilon : ℝ} (hepsilon : 0 < epsilon) :
  ∃ t c,
    ‖(∑ b ∈ t,
                c b •
                  ↑↑(MeasureTheory.fourierCharacterLpMultiplier j ⋯ b))
              f -
            (MeasureTheory.indicatorLp s hs) f‖ <
        epsilon ∧
      ‖(∑ b ∈ t,
                c b •
                  ↑↑(MeasureTheory.fourierCharacterLpMultiplier j ⋯ b))
              g -
            (MeasureTheory.indicatorLp s hs) g‖ <
        epsilon

theorem MeasureTheory.exists_finsetSum_fourierCharacterLpMultiplier_approx_indicatorLp.{u_1,
    u_2}
  {X : Type u_1} {V : Type u_2}
  [MeasurableSpace X]
  [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  {μ : MeasureTheory.Measure X}
  (j : X → V) (hj : MeasurableEmbedding j)
  (f g : ↥(MeasureTheory.Lp ℂ 2 μ))
  (s : Set X) (hs : MeasurableSet s)
  {epsilon : ℝ} (hepsilon : 0 < epsilon) :
  ∃ t c,
    ‖(∑ b ∈ t,
                c b •
                  ↑↑(MeasureTheory.fourierCharacterLpMultiplier
                        j ⋯ b))
              f -
            (MeasureTheory.indicatorLp s
                hs)
              f‖ <
        epsilon ∧
      ‖(∑ b ∈ t,
                c b •
                  ↑↑(MeasureTheory.fourierCharacterLpMultiplier
                        j ⋯ b))
              g -
            (MeasureTheory.indicatorLp s
                hs)
              g‖ <
        epsilon

A measurable indicator can be approximated simultaneously on two `L²` vectors by one finite
complex linear combination of pulled-back Fourier-character multipliers.

The proof pushes the finite measure weighted by the squared norms of `f` and `g` through `j`,
applies `exists_fourierCharacter_finset_approx_indicator_eLpNorm`, and pulls the approximation
back.  The simultaneous form is what allows the same polynomial to approximate both `f` and
`T f`.

theoremdefined in LeanRidgelet/ToMathlib/FourierCharacterMultiplier.lean

complete

theorem MeasureTheory.ContinuousLinearMap.commutes_finsetSum_fourierCharacterLpMultiplier.{u_1,
    u_2}
  {X : Type u_1} {V : Type u_2} [MeasurableSpace X]
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure X}
  (j : X → V) (hj : Measurable j)
  (T : ↥(MeasureTheory.Lp ℂ 2 μ) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 μ))
  (hchar :
    ∀ (b : V),
      T ∘SL ↑↑(MeasureTheory.fourierCharacterLpMultiplier j hj b) =
        ↑↑(MeasureTheory.fourierCharacterLpMultiplier j hj b) ∘SL T)
  (s : Finset V) (c : V → ℂ) :
  T ∘SL
      ∑ b ∈ s,
        c b • ↑↑(MeasureTheory.fourierCharacterLpMultiplier j hj b) =
    (∑ b ∈ s,
        c b • ↑↑(MeasureTheory.fourierCharacterLpMultiplier j hj b)) ∘SL
      T

theorem MeasureTheory.ContinuousLinearMap.commutes_finsetSum_fourierCharacterLpMultiplier.{u_1,
    u_2}
  {X : Type u_1} {V : Type u_2}
  [MeasurableSpace X]
  [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  {μ : MeasureTheory.Measure X}
  (j : X → V) (hj : Measurable j)
  (T :
    ↥(MeasureTheory.Lp ℂ 2 μ) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2 μ))
  (hchar :
    ∀ (b : V),
      T ∘SL
          ↑↑(MeasureTheory.fourierCharacterLpMultiplier
                j hj b) =
        ↑↑(MeasureTheory.fourierCharacterLpMultiplier
                j hj b) ∘SL
          T)
  (s : Finset V) (c : V → ℂ) :
  T ∘SL
      ∑ b ∈ s,
        c b •
          ↑↑(MeasureTheory.fourierCharacterLpMultiplier
                j hj b) =
    (∑ b ∈ s,
        c b •
          ↑↑(MeasureTheory.fourierCharacterLpMultiplier
                j hj b)) ∘SL
      T

Commutation with individual Fourier-character multipliers extends to every finite complex
linear combination of them.

theoremdefined in LeanRidgelet/ToMathlib/FourierCharacterMultiplier.lean

complete

theorem MeasureTheory.ContinuousLinearMap.commutes_indicatorLp_of_commutes_fourierCharacter.{u_1,
    u_2}
  {X : Type u_1} {V : Type u_2} [MeasurableSpace X]
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure X}
  (j : X → V) (hj : MeasurableEmbedding j)
  (T : ↥(MeasureTheory.Lp ℂ 2 μ) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 μ))
  (hchar :
    ∀ (b : V),
      T ∘SL ↑↑(MeasureTheory.fourierCharacterLpMultiplier j ⋯ b) =
        ↑↑(MeasureTheory.fourierCharacterLpMultiplier j ⋯ b) ∘SL T)
  (s : Set X) (hs : MeasurableSet s) :
  T ∘SL MeasureTheory.indicatorLp s hs =
    MeasureTheory.indicatorLp s hs ∘SL T

theorem MeasureTheory.ContinuousLinearMap.commutes_indicatorLp_of_commutes_fourierCharacter.{u_1,
    u_2}
  {X : Type u_1} {V : Type u_2}
  [MeasurableSpace X]
  [NormedAddCommGroup V]
  [InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V]
  {μ : MeasureTheory.Measure X}
  (j : X → V) (hj : MeasurableEmbedding j)
  (T :
    ↥(MeasureTheory.Lp ℂ 2 μ) →L[ℂ]
      ↥(MeasureTheory.Lp ℂ 2 μ))
  (hchar :
    ∀ (b : V),
      T ∘SL
          ↑↑(MeasureTheory.fourierCharacterLpMultiplier
                j ⋯ b) =
        ↑↑(MeasureTheory.fourierCharacterLpMultiplier
                j ⋯ b) ∘SL
          T)
  (s : Set X) (hs : MeasurableSet s) :
  T ∘SL MeasureTheory.indicatorLp s hs =
    MeasureTheory.indicatorLp s hs ∘SL T

A bounded operator commuting with every pulled-back Fourier-character multiplier commutes
with every measurable indicator projection.

This is the minimal `L²` multiplier consequence of the spectral-projection commutant criterion:
the measurable embedding ensures that the restricted characters generate the measurable
structure on `X`.  No general projection-valued-measure object is needed.

Product measures

Theorem5.1.14

uses 0

Used by 2

Reverse dependency previews

Preview

Lemma 2.2.7

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Parametrized shears and rearrangements of product measures. Two elementary transports for iterated Fubini arguments: the rearrangement ((a,b),c)\mapsto((a,c),b) exchanging the two right factors of a left-nested triple product of s-finite measures preserves the product measures; and for a measurable parameter map c into a measurable group with an invariant fiber measure, the parametrized shears (w,b)\mapsto(w,c(w)/b) and (w,b)\mapsto(w,b/c(w)) preserve μ.prod ν, with quasi-measure-preserving evaluations (w,b)\mapsto c(w)/b and (w,b)\mapsto b/c(w) (multiplicative and additive versions). The evaluations are the standard device for the joint measurability of kernels (w,b)\mapsto g(c(w)-b) with g merely a.e. strongly measurable.

Lean code for Theorem5.1.14●9 theorems

theoremdefined in LeanRidgelet/ToMathlib/ProdShear.lean

complete

theorem MeasureTheory.measurePreserving_prodSwapRight.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] [MeasurableSpace γ] (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure β) (ρ : MeasureTheory.Measure γ)
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν]
  [MeasureTheory.SFinite ρ] :
  MeasureTheory.MeasurePreserving (fun q ↦ ((q.1.1, q.2), q.1.2))
    ((μ.prod ν).prod ρ) ((μ.prod ρ).prod ν)

theorem MeasureTheory.measurePreserving_prodSwapRight.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {γ : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] [MeasurableSpace γ]
  (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure β)
  (ρ : MeasureTheory.Measure γ)
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  [MeasureTheory.SFinite ρ] :
  MeasureTheory.MeasurePreserving
    (fun q ↦ ((q.1.1, q.2), q.1.2))
    ((μ.prod ν).prod ρ)
    ((μ.prod ρ).prod ν)

The rearrangement `((a, b), c) ↦ ((a, c), b)` exchanging the two right factors of a
left-nested triple product preserves the product measures.

theoremdefined in LeanRidgelet/ToMathlib/ProdShear.lean

complete

theorem MeasureTheory.measurePreserving_skewDivLeft.{u_1, u_4} {α : Type u_1}
  [MeasurableSpace α] {G : Type u_4} [MeasurableSpace G] [Group G]
  [MeasurableMul₂ G] [MeasurableInv G] (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] [ν.IsMulLeftInvariant] [ν.IsInvInvariant]
  {c : α → G} (hc : Measurable c) :
  MeasureTheory.MeasurePreserving (fun q ↦ (q.1, c q.1 / q.2))
    (μ.prod ν) (μ.prod ν)

theorem MeasureTheory.measurePreserving_skewDivLeft.{u_1,
    u_4}
  {α : Type u_1} [MeasurableSpace α]
  {G : Type u_4} [MeasurableSpace G]
  [Group G] [MeasurableMul₂ G]
  [MeasurableInv G]
  (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  [ν.IsMulLeftInvariant]
  [ν.IsInvInvariant] {c : α → G}
  (hc : Measurable c) :
  MeasureTheory.MeasurePreserving
    (fun q ↦ (q.1, c q.1 / q.2))
    (μ.prod ν) (μ.prod ν)

The parametrized shear `(w, b) ↦ (w, c w / b)` preserves the product with an inversion-
and left-invariant fiber measure.

theoremdefined in LeanRidgelet/ToMathlib/ProdShear.lean

complete

theorem MeasureTheory.measurePreserving_skewSubLeft.{u_1, u_4} {α : Type u_1}
  [MeasurableSpace α] {G : Type u_4} [MeasurableSpace G] [AddGroup G]
  [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] [ν.IsAddLeftInvariant] [ν.IsNegInvariant]
  {c : α → G} (hc : Measurable c) :
  MeasureTheory.MeasurePreserving (fun q ↦ (q.1, c q.1 - q.2))
    (μ.prod ν) (μ.prod ν)

theorem MeasureTheory.measurePreserving_skewSubLeft.{u_1,
    u_4}
  {α : Type u_1} [MeasurableSpace α]
  {G : Type u_4} [MeasurableSpace G]
  [AddGroup G] [MeasurableAdd₂ G]
  [MeasurableNeg G]
  (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  [ν.IsAddLeftInvariant]
  [ν.IsNegInvariant] {c : α → G}
  (hc : Measurable c) :
  MeasureTheory.MeasurePreserving
    (fun q ↦ (q.1, c q.1 - q.2))
    (μ.prod ν) (μ.prod ν)

The parametrized shear `(w, b) ↦ (w, c w - b)` preserves the product with a negation-
and left-invariant fiber measure.

theoremdefined in LeanRidgelet/ToMathlib/ProdShear.lean

complete

theorem MeasureTheory.quasiMeasurePreserving_skewDivLeft.{u_1, u_4}
  {α : Type u_1} [MeasurableSpace α] {G : Type u_4} [MeasurableSpace G]
  [Group G] [MeasurableMul₂ G] [MeasurableInv G]
  (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν]
  [ν.IsMulLeftInvariant] [ν.IsInvInvariant] {c : α → G}
  (hc : Measurable c) :
  MeasureTheory.Measure.QuasiMeasurePreserving (fun q ↦ c q.1 / q.2)
    (μ.prod ν) ν

theorem MeasureTheory.quasiMeasurePreserving_skewDivLeft.{u_1,
    u_4}
  {α : Type u_1} [MeasurableSpace α]
  {G : Type u_4} [MeasurableSpace G]
  [Group G] [MeasurableMul₂ G]
  [MeasurableInv G]
  (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  [ν.IsMulLeftInvariant]
  [ν.IsInvInvariant] {c : α → G}
  (hc : Measurable c) :
  MeasureTheory.Measure.QuasiMeasurePreserving
    (fun q ↦ c q.1 / q.2) (μ.prod ν) ν

The parametrized evaluation `(w, b) ↦ c w / b` is quasi-measure-preserving from a product
with an inversion- and left-invariant fiber measure to the fiber. This is the standard device
for the joint measurability of kernels `(w, b) ↦ g (c w / b)` with `g` merely a.e. strongly
measurable.

theoremdefined in LeanRidgelet/ToMathlib/ProdShear.lean

complete

theorem MeasureTheory.quasiMeasurePreserving_skewSubLeft.{u_1, u_4}
  {α : Type u_1} [MeasurableSpace α] {G : Type u_4} [MeasurableSpace G]
  [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G]
  (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν]
  [ν.IsAddLeftInvariant] [ν.IsNegInvariant] {c : α → G}
  (hc : Measurable c) :
  MeasureTheory.Measure.QuasiMeasurePreserving (fun q ↦ c q.1 - q.2)
    (μ.prod ν) ν

theorem MeasureTheory.quasiMeasurePreserving_skewSubLeft.{u_1,
    u_4}
  {α : Type u_1} [MeasurableSpace α]
  {G : Type u_4} [MeasurableSpace G]
  [AddGroup G] [MeasurableAdd₂ G]
  [MeasurableNeg G]
  (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  [ν.IsAddLeftInvariant]
  [ν.IsNegInvariant] {c : α → G}
  (hc : Measurable c) :
  MeasureTheory.Measure.QuasiMeasurePreserving
    (fun q ↦ c q.1 - q.2) (μ.prod ν) ν

The parametrized evaluation `(w, b) ↦ c w - b` is quasi-measure-preserving from a
product with a negation- and left-invariant fiber measure to the fiber. This is the standard
device for the joint measurability of kernels `(w, b) ↦ g (c w - b)` with `g` merely a.e.
strongly measurable.

theoremdefined in LeanRidgelet/ToMathlib/ProdShear.lean

complete

theorem MeasureTheory.measurePreserving_skewDivRight.{u_1, u_4} {α : Type u_1}
  [MeasurableSpace α] {G : Type u_4} [MeasurableSpace G] [Group G]
  [MeasurableMul₂ G] [MeasurableInv G] (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] [ν.IsMulRightInvariant] {c : α → G}
  (hc : Measurable c) :
  MeasureTheory.MeasurePreserving (fun q ↦ (q.1, q.2 / c q.1))
    (μ.prod ν) (μ.prod ν)

theorem MeasureTheory.measurePreserving_skewDivRight.{u_1,
    u_4}
  {α : Type u_1} [MeasurableSpace α]
  {G : Type u_4} [MeasurableSpace G]
  [Group G] [MeasurableMul₂ G]
  [MeasurableInv G]
  (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  [ν.IsMulRightInvariant] {c : α → G}
  (hc : Measurable c) :
  MeasureTheory.MeasurePreserving
    (fun q ↦ (q.1, q.2 / c q.1))
    (μ.prod ν) (μ.prod ν)

The parametrized shear `(w, b) ↦ (w, b / c w)` preserves the product with a
right-invariant fiber measure.

theoremdefined in LeanRidgelet/ToMathlib/ProdShear.lean

complete

theorem MeasureTheory.measurePreserving_skewSubRight.{u_1, u_4} {α : Type u_1}
  [MeasurableSpace α] {G : Type u_4} [MeasurableSpace G] [AddGroup G]
  [MeasurableAdd₂ G] [MeasurableNeg G] (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure G) [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] [ν.IsAddRightInvariant] {c : α → G}
  (hc : Measurable c) :
  MeasureTheory.MeasurePreserving (fun q ↦ (q.1, q.2 - c q.1))
    (μ.prod ν) (μ.prod ν)

theorem MeasureTheory.measurePreserving_skewSubRight.{u_1,
    u_4}
  {α : Type u_1} [MeasurableSpace α]
  {G : Type u_4} [MeasurableSpace G]
  [AddGroup G] [MeasurableAdd₂ G]
  [MeasurableNeg G]
  (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  [ν.IsAddRightInvariant] {c : α → G}
  (hc : Measurable c) :
  MeasureTheory.MeasurePreserving
    (fun q ↦ (q.1, q.2 - c q.1))
    (μ.prod ν) (μ.prod ν)

The parametrized shear `(w, b) ↦ (w, b - c w)` preserves the product with a
right-invariant fiber measure.

theoremdefined in LeanRidgelet/ToMathlib/ProdShear.lean

complete

theorem MeasureTheory.quasiMeasurePreserving_skewDivRight.{u_1, u_4}
  {α : Type u_1} [MeasurableSpace α] {G : Type u_4} [MeasurableSpace G]
  [Group G] [MeasurableMul₂ G] [MeasurableInv G]
  (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν]
  [ν.IsMulRightInvariant] {c : α → G} (hc : Measurable c) :
  MeasureTheory.Measure.QuasiMeasurePreserving (fun q ↦ q.2 / c q.1)
    (μ.prod ν) ν

theorem MeasureTheory.quasiMeasurePreserving_skewDivRight.{u_1,
    u_4}
  {α : Type u_1} [MeasurableSpace α]
  {G : Type u_4} [MeasurableSpace G]
  [Group G] [MeasurableMul₂ G]
  [MeasurableInv G]
  (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  [ν.IsMulRightInvariant] {c : α → G}
  (hc : Measurable c) :
  MeasureTheory.Measure.QuasiMeasurePreserving
    (fun q ↦ q.2 / c q.1) (μ.prod ν) ν

The parametrized evaluation `(w, b) ↦ b / c w` is quasi-measure-preserving from a product
with a right-invariant fiber measure to the fiber.

theoremdefined in LeanRidgelet/ToMathlib/ProdShear.lean

complete

theorem MeasureTheory.quasiMeasurePreserving_skewSubRight.{u_1, u_4}
  {α : Type u_1} [MeasurableSpace α] {G : Type u_4} [MeasurableSpace G]
  [AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G]
  (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν]
  [ν.IsAddRightInvariant] {c : α → G} (hc : Measurable c) :
  MeasureTheory.Measure.QuasiMeasurePreserving (fun q ↦ q.2 - c q.1)
    (μ.prod ν) ν

theorem MeasureTheory.quasiMeasurePreserving_skewSubRight.{u_1,
    u_4}
  {α : Type u_1} [MeasurableSpace α]
  {G : Type u_4} [MeasurableSpace G]
  [AddGroup G] [MeasurableAdd₂ G]
  [MeasurableNeg G]
  (μ : MeasureTheory.Measure α)
  (ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  [ν.IsAddRightInvariant] {c : α → G}
  (hc : Measurable c) :
  MeasureTheory.Measure.QuasiMeasurePreserving
    (fun q ↦ q.2 - c q.1) (μ.prod ν) ν

The parametrized evaluation `(w, b) ↦ b - c w` is quasi-measure-preserving from a
product with a right-invariant fiber measure to the fiber.

Relatively invariant densities and the congruence determinant

Theorem5.1.15

uses 1used by 1✓L∃∀N

Weighting a relatively invariant measure. If a map scales a measure by a constant and scales a weight by a constant, it scales the weighted measure by the product of the two reciprocals; and restricting to an invariant set changes nothing.

Lean code for Theorem5.1.15●2 theorems

theoremdefined in LeanRidgelet/ToMathlib/RelativelyInvariantDensity.lean

complete

theorem MeasureTheory.Measure.map_withDensity_of_map_eq_smul.{u_1}
  {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X}
  {T : X → X} {w : X → ENNReal} {c κ : ENNReal} (hT : Measurable T)
  (hw : Measurable w) (hmap : MeasureTheory.Measure.map T μ = c • μ)
  (hweight : ∀ (x : X), w (T x) = κ * w x) (hκ : κ ≠ 0) (hκ' : κ ≠ ⊤) :
  MeasureTheory.Measure.map T (μ.withDensity w) =
    (κ⁻¹ * c) • μ.withDensity w

theorem MeasureTheory.Measure.map_withDensity_of_map_eq_smul.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  {T : X → X} {w : X → ENNReal}
  {c κ : ENNReal} (hT : Measurable T)
  (hw : Measurable w)
  (hmap :
    MeasureTheory.Measure.map T μ = c • μ)
  (hweight : ∀ (x : X), w (T x) = κ * w x)
  (hκ : κ ≠ 0) (hκ' : κ ≠ ⊤) :
  MeasureTheory.Measure.map T
      (μ.withDensity w) =
    (κ⁻¹ * c) • μ.withDensity w

Pushforward of a weighted measure by a map that rescales both the base measure and the
weight.  If `T` sends `μ` to `c • μ` and multiplies the weight `w` by the constant `κ`, then it
sends `μ.withDensity w` to `(κ⁻¹ * c) • μ.withDensity w`.  The constant `κ` must be neither zero
nor infinite so that it can be divided out.

theoremdefined in LeanRidgelet/ToMathlib/RelativelyInvariantDensity.lean

complete

theorem MeasureTheory.Measure.map_restrict_of_map_eq_smul.{u_1} {X : Type u_1}
  [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → X}
  {c : ENNReal} {s : Set X} (hT : Measurable T)
  (hmap : MeasureTheory.Measure.map T μ = c • μ) (hs : MeasurableSet s)
  (hinv : T ⁻¹' s = s) :
  MeasureTheory.Measure.map T (μ.restrict s) = c • μ.restrict s

theorem MeasureTheory.Measure.map_restrict_of_map_eq_smul.{u_1}
  {X : Type u_1} [MeasurableSpace X]
  {μ : MeasureTheory.Measure X}
  {T : X → X} {c : ENNReal} {s : Set X}
  (hT : Measurable T)
  (hmap :
    MeasureTheory.Measure.map T μ = c • μ)
  (hs : MeasurableSet s)
  (hinv : T ⁻¹' s = s) :
  MeasureTheory.Measure.map T
      (μ.restrict s) =
    c • μ.restrict s

Restricting to a set invariant under `T` preserves the rescaling law `μ.map T = c • μ`.

The two statements are what turn a relative invariant of a group action into a parameter measure with a prescribed density. The first is stated for an arbitrary measure and an arbitrary scaling, not for a Haar measure and a linear automorphism, precisely so that the second can be composed with it: one restricts a Haar measure to the invariant complement of a degenerate locus, which keeps the scaling, and then weights it.

Theorem5.1.16

uses 0used by 1✓L∃∀N

The determinant of congruence. On the symmetric matrices of size n, the map A\mapsto M^\top AM has determinant (\det M)^{n+1}; equivalently, on the self-adjoint endomorphisms of a finite-dimensional real inner product space, congruence has determinant the dimension-plus-one power of the determinant.

Lean code for Theorem5.1.16●10 declarations

defdefined in LeanRidgelet/ToMathlib/SymmetricCongruenceDet.lean

complete

def Matrix.symmetricSubmodule (n : ℕ) :
  Submodule ℝ (Matrix (Fin n) (Fin n) ℝ)

def Matrix.symmetricSubmodule (n : ℕ) :
  Submodule ℝ (Matrix (Fin n) (Fin n) ℝ)

Implementation after :=

:= {A | A.IsSymm}
  add_mem' hA hB := hA.add hB
  zero_mem' := isSymm_zero
  smul_mem' c _ hA := hA.smul c

The symmetric matrices, as a submodule of all matrices.

defdefined in LeanRidgelet/ToMathlib/SymmetricCongruenceDet.lean

complete

def Matrix.symmetricBasis (n : ℕ) :
  Module.Basis (Matrix.SymIdx n) ℝ ↥(Matrix.symmetricSubmodule n)

def Matrix.symmetricBasis (n : ℕ) :
  Module.Basis (Matrix.SymIdx n) ℝ
    ↥(Matrix.symmetricSubmodule n)

Implementation after :=

:=
  Basis.ofEquivFun (symmetricEquivFun n)

The basis of the symmetric matrices indexed by the pairs `(i, j)` with `i ≤ j`: the basis
vector at `(i, i)` is `Matrix.single i i 1`, and the one at `(i, j)` with `i < j` is
`Matrix.single i j 1 + Matrix.single j i 1`.

defdefined in LeanRidgelet/ToMathlib/SymmetricCongruenceDet.lean

complete

def Matrix.congrMap {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ) :
  ↥(Matrix.symmetricSubmodule n) →ₗ[ℝ] ↥(Matrix.symmetricSubmodule n)

def Matrix.congrMap {n : ℕ}
  (M : Matrix (Fin n) (Fin n) ℝ) :
  ↥(Matrix.symmetricSubmodule n) →ₗ[ℝ]
    ↥(Matrix.symmetricSubmodule n)

Implementation after :=

:= ⟨Mᵀ * (A : Matrix (Fin n) (Fin n) ℝ) * M, by
    change (Mᵀ * (A : Matrix (Fin n) (Fin n) ℝ) * M).IsSymm
    simp only [IsSymm, transpose_mul, transpose_transpose, (isSymm_coe A).eq, Matrix.mul_assoc]⟩
  map_add' A B := by ext i j; simp [Matrix.mul_add, Matrix.add_mul]
  map_smul' c A := by ext i j; simp

Congruence by `M`, that is `A ↦ Mᵀ * A * M`, as an endomorphism of the symmetric matrices.

theoremdefined in LeanRidgelet/ToMathlib/SymmetricCongruenceDet.lean

complete

theorem Matrix.congrMap_mul {n : ℕ} (M N : Matrix (Fin n) (Fin n) ℝ) :
  (M * N).congrMap = N.congrMap ∘ₗ M.congrMap

theorem Matrix.congrMap_mul {n : ℕ}
  (M N : Matrix (Fin n) (Fin n) ℝ) :
  (M * N).congrMap =
    N.congrMap ∘ₗ M.congrMap

Congruence is an anti-homomorphism: `congrMap (M * N) = congrMap N ∘ congrMap M`.

theoremdefined in LeanRidgelet/ToMathlib/SymmetricCongruenceDet.lean

complete

theorem Matrix.det_congrMap_diagonal {n : ℕ} (d : Fin n → ℝ) :
  LinearMap.det (Matrix.diagonal d).congrMap =
    (Matrix.diagonal d).det ^ (n + 1)

theorem Matrix.det_congrMap_diagonal {n : ℕ}
  (d : Fin n → ℝ) :
  LinearMap.det
      (Matrix.diagonal d).congrMap =
    (Matrix.diagonal d).det ^ (n + 1)

theoremdefined in LeanRidgelet/ToMathlib/SymmetricCongruenceDet.lean

complete

theorem Matrix.det_congrMap_transvection {n : ℕ} {i j : Fin n} (hij : i ≠ j)
  (c : ℝ) : LinearMap.det (Matrix.transvection i j c).congrMap = 1

theorem Matrix.det_congrMap_transvection {n : ℕ}
  {i j : Fin n} (hij : i ≠ j) (c : ℝ) :
  LinearMap.det
      (Matrix.transvection i j
          c).congrMap =
    1

**Congruence by a transvection has determinant one.**

Write `f e` for the determinant of congruence by `transvection i j e`.  Adding the parameters
multiplies the determinants, so `f (2 * c) = f c ^ 2`; conjugating by the diagonal matrix with a
single entry `2` doubles the parameter without changing the determinant, so `f (2 * c) = f c`.
Since `f c ≠ 0`, these force `f c = 1`.

theoremdefined in LeanRidgelet/ToMathlib/SymmetricCongruenceDet.lean

complete

theorem Matrix.det_congrMap {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ) :
  LinearMap.det M.congrMap = M.det ^ (n + 1)

theorem Matrix.det_congrMap {n : ℕ}
  (M : Matrix (Fin n) (Fin n) ℝ) :
  LinearMap.det M.congrMap =
    M.det ^ (n + 1)

**The determinant of congruence on symmetric matrices.**  Congruence by `M`, that is
`A ↦ Mᵀ * A * M`, acts on the `n (n + 1) / 2`-dimensional space of symmetric `n × n` matrices
with determinant `(det M) ^ (n + 1)`.

defdefined in LeanRidgelet/ToMathlib/SymmetricCongruenceDet.lean

complete

def ContinuousLinearMap.congrSelfAdjoint.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (M : E →L[ℝ] E) :
  ↥(selfAdjoint (E →L[ℝ] E)) →ₗ[ℝ] ↥(selfAdjoint (E →L[ℝ] E))

def ContinuousLinearMap.congrSelfAdjoint.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (M : E →L[ℝ] E) :
  ↥(selfAdjoint (E →L[ℝ] E)) →ₗ[ℝ]
    ↥(selfAdjoint (E →L[ℝ] E))

Implementation after :=

:= ⟨star M * (A : E →L[ℝ] E) * M, A.2.conjugate' M⟩
  map_add' A B := by refine Subtype.ext ?_; simp [mul_add, add_mul]
  map_smul' c A := by refine Subtype.ext ?_; simp

Congruence `A ↦ star M * A * M`, that is `A ↦ Mᵀ A M` with the adjoint for transpose, as an
endomorphism of the self-adjoint continuous endomorphisms of `E`.

defdefined in LeanRidgelet/ToMathlib/SymmetricCongruenceDet.lean

complete

def ContinuousLinearMap.selfAdjointEquivSymmetric.{u_2} (E : Type u_2)
  [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  ↥(selfAdjoint (E →L[ℝ] E)) ≃ₗ[ℝ]
    ↥(Matrix.symmetricSubmodule (Module.finrank ℝ E))

def ContinuousLinearMap.selfAdjointEquivSymmetric.{u_2}
  (E : Type u_2) [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] :
  ↥(selfAdjoint (E →L[ℝ] E)) ≃ₗ[ℝ]
    ↥(Matrix.symmetricSubmodule
        (Module.finrank ℝ E))

Implementation after :=

:= ⟨toMatrixStarAlgEquiv E A, isSymm_toMatrixStarAlgEquiv A.2⟩
  invFun B := ⟨(toMatrixStarAlgEquiv E).symm B, isSelfAdjoint_symm_toMatrixStarAlgEquiv B.2⟩
  map_add' A B := by refine Subtype.ext ?_; simp
  map_smul' c A := by refine Subtype.ext ?_; simp
  left_inv A := by refine Subtype.ext ?_; simp
  right_inv B := by refine Subtype.ext ?_; simp

Under the standard orthonormal basis the self-adjoint continuous endomorphisms of `E`
correspond to the symmetric matrices of size `finrank ℝ E`.

theoremdefined in LeanRidgelet/ToMathlib/SymmetricCongruenceDet.lean

complete

theorem ContinuousLinearMap.det_congrSelfAdjoint.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (M : E →L[ℝ] E) :
  LinearMap.det M.congrSelfAdjoint = M.det ^ (Module.finrank ℝ E + 1)

theorem ContinuousLinearMap.det_congrSelfAdjoint.{u_1}
  {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E]
  (M : E →L[ℝ] E) :
  LinearMap.det M.congrSelfAdjoint =
    M.det ^ (Module.finrank ℝ E + 1)

**The determinant of congruence on self-adjoint operators.**  For `M : E →L[ℝ] E` on a
finite-dimensional real inner product space, the congruence `A ↦ star M * A * M` on the
self-adjoint endomorphisms has determinant `M.det ^ (finrank ℝ E + 1)`.

A `Submodule ℝ (E →L[ℝ] E)` carved out by `IsSelfAdjoint` carries the same coercion to a type and
the same `ℝ`-module structure as `selfAdjoint (E →L[ℝ] E)`, definitionally; the identity map is a
`LinearEquiv` between the two with `rfl` for all four proof fields, so this statement transports
to such a formulation without work.

Mathlib has the symmetric matrices as a predicate but not as a subspace, so the subspace, its basis indexed by the pairs i ≤ j, and the congruence map are built here. Congruence is an anti-homomorphism, so its determinant is multiplicative, and it suffices to compute on the generators of the invertible matrices. On a diagonal matrix the basis is an eigenbasis with eigenvalues the products of the two diagonal entries, and each index occurs in n + 1 of those products, which gives the exponent. On a transvection the determinant is one, by an argument that avoids both nilpotence and continuity: conjugating a transvection by a diagonal matrix rescales its parameter, so the determinant is invariant under doubling the parameter, while it is also multiplicative in it; being nonzero, it is one. The singular case needs no generators: a vector killed by the transpose produces a nonzero symmetric matrix in the kernel, so both sides vanish. The basis-free form is transported along an orthonormal basis, under which the adjoint becomes the transpose and self-adjointness becomes symmetry.

Factoring a Haar measure over the last coordinate

Theorem5.1.17

uses 1used by 1✓L∃∀N

Reassociating a triple product. An additive Haar measure on a right-nested triple product becomes, after the associativity transport, a positive finite multiple of a product of additive Haar measures; and restricting to a set that reads only the first two coordinates, or weighting by a density that reads only those, commutes with the transport.

Lean code for Theorem5.1.17●5 theorems

theoremdefined in LeanRidgelet/ToMathlib/HaarProdAssoc.lean

complete

theorem MeasureTheory.Measure.map_withDensity_measurableEquiv.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  (μ : MeasureTheory.Measure α) (e : α ≃ᵐ β) {w : β → ENNReal}
  (hw : Measurable w) :
  MeasureTheory.Measure.map (⇑e) (μ.withDensity fun x ↦ w (e x)) =
    (MeasureTheory.Measure.map (⇑e) μ).withDensity w

theorem MeasureTheory.Measure.map_withDensity_measurableEquiv.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  (μ : MeasureTheory.Measure α)
  (e : α ≃ᵐ β) {w : β → ENNReal}
  (hw : Measurable w) :
  MeasureTheory.Measure.map (⇑e)
      (μ.withDensity fun x ↦ w (e x)) =
    (MeasureTheory.Measure.map (⇑e)
          μ).withDensity
      w

Pushing a weighted measure forward along a measurable equivalence weights the pushforward by
the transported density.  Both sides are evaluated on a measurable set, where the identity is the
change of variables for the lower Lebesgue integral of an indicator.

theoremdefined in LeanRidgelet/ToMathlib/HaarProdAssoc.lean

complete

theorem MeasureTheory.Measure.exists_map_prodAssoc_symm_eq_smul_prod.{u_3, u_4,
    u_5}
  {X : Type u_3} {Y : Type u_4} {Z : Type u_5} [AddGroup X]
  [TopologicalSpace X] [IsTopologicalAddGroup X] [MeasurableSpace X]
  [BorelSpace X] [SecondCountableTopology X] [LocallyCompactSpace X]
  [AddGroup Y] [TopologicalSpace Y] [IsTopologicalAddGroup Y]
  [MeasurableSpace Y] [BorelSpace Y] [SecondCountableTopology Y]
  [LocallyCompactSpace Y] [AddGroup Z] [TopologicalSpace Z]
  [IsTopologicalAddGroup Z] [MeasurableSpace Z] [BorelSpace Z]
  [SecondCountableTopology Z] [LocallyCompactSpace Z]
  (lam : MeasureTheory.Measure (X × Y × Z)) [lam.IsAddHaarMeasure]
  (κ : MeasureTheory.Measure (X × Y)) [κ.IsAddHaarMeasure]
  (ν : MeasureTheory.Measure Z) [ν.IsAddHaarMeasure] :
  ∃ c,
    c ≠ 0 ∧
      c ≠ ⊤ ∧
        MeasureTheory.Measure.map (⇑MeasurableEquiv.prodAssoc.symm)
            lam =
          c • κ.prod ν

theorem MeasureTheory.Measure.exists_map_prodAssoc_symm_eq_smul_prod.{u_3,
    u_4, u_5}
  {X : Type u_3} {Y : Type u_4}
  {Z : Type u_5} [AddGroup X]
  [TopologicalSpace X]
  [IsTopologicalAddGroup X]
  [MeasurableSpace X] [BorelSpace X]
  [SecondCountableTopology X]
  [LocallyCompactSpace X] [AddGroup Y]
  [TopologicalSpace Y]
  [IsTopologicalAddGroup Y]
  [MeasurableSpace Y] [BorelSpace Y]
  [SecondCountableTopology Y]
  [LocallyCompactSpace Y] [AddGroup Z]
  [TopologicalSpace Z]
  [IsTopologicalAddGroup Z]
  [MeasurableSpace Z] [BorelSpace Z]
  [SecondCountableTopology Z]
  [LocallyCompactSpace Z]
  (lam :
    MeasureTheory.Measure (X × Y × Z))
  [lam.IsAddHaarMeasure]
  (κ : MeasureTheory.Measure (X × Y))
  [κ.IsAddHaarMeasure]
  (ν : MeasureTheory.Measure Z)
  [ν.IsAddHaarMeasure] :
  ∃ c,
    c ≠ 0 ∧
      c ≠ ⊤ ∧
        MeasureTheory.Measure.map
            (⇑MeasurableEquiv.prodAssoc.symm)
            lam =
          c • κ.prod ν

**An additive Haar measure on a right-nested triple product is a multiple of a product.**
After transport along the associativity equivalence, an additive Haar measure `lam` on `X × Y × Z`
is a positive finite multiple of the product of additive Haar measures `κ` on `X × Y` and `ν` on
`Z`.  The constant depends on the three measures and is not otherwise determined.

theoremdefined in LeanRidgelet/ToMathlib/HaarProdAssoc.lean

complete

theorem MeasureTheory.Measure.preimage_prodAssoc_symm_prod_univ.{u_3, u_4, u_5}
  {X : Type u_3} {Y : Type u_4} {Z : Type u_5} [MeasurableSpace X]
  [MeasurableSpace Y] [MeasurableSpace Z] (t : Set (X × Y)) :
  ⇑MeasurableEquiv.prodAssoc.symm ⁻¹' t ×ˢ Set.univ =
    {p | (p.1, p.2.1) ∈ t}

theorem MeasureTheory.Measure.preimage_prodAssoc_symm_prod_univ.{u_3,
    u_4, u_5}
  {X : Type u_3} {Y : Type u_4}
  {Z : Type u_5} [MeasurableSpace X]
  [MeasurableSpace Y] [MeasurableSpace Z]
  (t : Set (X × Y)) :
  ⇑MeasurableEquiv.prodAssoc.symm ⁻¹'
      t ×ˢ Set.univ =
    {p | (p.1, p.2.1) ∈ t}

The set `{p | (p.1, p.2.1) ∈ t}` of a right-nested triple product, for `t` a set of the
left-nested pair, is exactly the preimage of the cylinder `t ×ˢ univ` under the associativity
equivalence.  This is the bookkeeping that makes the two commutation lemmas below apply.

theoremdefined in LeanRidgelet/ToMathlib/HaarProdAssoc.lean

complete

theorem MeasureTheory.Measure.map_prodAssoc_symm_restrict_of_map_eq_smul.{u_3,
    u_4, u_5}
  {X : Type u_3} {Y : Type u_4} {Z : Type u_5} [MeasurableSpace X]
  [MeasurableSpace Y] [MeasurableSpace Z]
  {μ : MeasureTheory.Measure (X × Y × Z)}
  {κ : MeasureTheory.Measure (X × Y)} {ν : MeasureTheory.Measure Z}
  [MeasureTheory.SFinite κ] [MeasureTheory.SFinite ν] {c : ENNReal}
  {t : Set (X × Y)} (ht : MeasurableSet t)
  (h :
    MeasureTheory.Measure.map (⇑MeasurableEquiv.prodAssoc.symm) μ =
      c • κ.prod ν) :
  MeasureTheory.Measure.map (⇑MeasurableEquiv.prodAssoc.symm)
      (μ.restrict {p | (p.1, p.2.1) ∈ t}) =
    c • (κ.restrict t).prod ν

theorem MeasureTheory.Measure.map_prodAssoc_symm_restrict_of_map_eq_smul.{u_3,
    u_4, u_5}
  {X : Type u_3} {Y : Type u_4}
  {Z : Type u_5} [MeasurableSpace X]
  [MeasurableSpace Y] [MeasurableSpace Z]
  {μ : MeasureTheory.Measure (X × Y × Z)}
  {κ : MeasureTheory.Measure (X × Y)}
  {ν : MeasureTheory.Measure Z}
  [MeasureTheory.SFinite κ]
  [MeasureTheory.SFinite ν] {c : ENNReal}
  {t : Set (X × Y)} (ht : MeasurableSet t)
  (h :
    MeasureTheory.Measure.map
        (⇑MeasurableEquiv.prodAssoc.symm)
        μ =
      c • κ.prod ν) :
  MeasureTheory.Measure.map
      (⇑MeasurableEquiv.prodAssoc.symm)
      (μ.restrict
        {p | (p.1, p.2.1) ∈ t}) =
    c • (κ.restrict t).prod ν

**Restriction through the first two factors commutes with the transport.**  If a measure `μ` on
`X × Y × Z` transports to `c • κ.prod ν`, then its restriction to a set constraining only the `X`
and `Y` coordinates transports to `c • (κ.restrict t).prod ν`.

theoremdefined in LeanRidgelet/ToMathlib/HaarProdAssoc.lean

complete

theorem MeasureTheory.Measure.map_prodAssoc_symm_withDensity_of_map_eq_smul.{u_3,
    u_4, u_5}
  {X : Type u_3} {Y : Type u_4} {Z : Type u_5} [MeasurableSpace X]
  [MeasurableSpace Y] [MeasurableSpace Z]
  {μ : MeasureTheory.Measure (X × Y × Z)}
  {κ : MeasureTheory.Measure (X × Y)} {ν : MeasureTheory.Measure Z}
  [MeasureTheory.SFinite ν] {c : ENNReal} {w : X × Y → ENNReal}
  (hw : Measurable w)
  (h :
    MeasureTheory.Measure.map (⇑MeasurableEquiv.prodAssoc.symm) μ =
      c • κ.prod ν) :
  MeasureTheory.Measure.map (⇑MeasurableEquiv.prodAssoc.symm)
      (μ.withDensity fun p ↦ w (p.1, p.2.1)) =
    c • (κ.withDensity w).prod ν

theorem MeasureTheory.Measure.map_prodAssoc_symm_withDensity_of_map_eq_smul.{u_3,
    u_4, u_5}
  {X : Type u_3} {Y : Type u_4}
  {Z : Type u_5} [MeasurableSpace X]
  [MeasurableSpace Y] [MeasurableSpace Z]
  {μ : MeasureTheory.Measure (X × Y × Z)}
  {κ : MeasureTheory.Measure (X × Y)}
  {ν : MeasureTheory.Measure Z}
  [MeasureTheory.SFinite ν] {c : ENNReal}
  {w : X × Y → ENNReal}
  (hw : Measurable w)
  (h :
    MeasureTheory.Measure.map
        (⇑MeasurableEquiv.prodAssoc.symm)
        μ =
      c • κ.prod ν) :
  MeasureTheory.Measure.map
      (⇑MeasurableEquiv.prodAssoc.symm)
      (μ.withDensity fun p ↦
        w (p.1, p.2.1)) =
    c • (κ.withDensity w).prod ν

**Weighting through the first two factors commutes with the transport.**  If a measure `μ` on
`X × Y × Z` transports to `c • κ.prod ν`, then weighting it by a density that reads only the `X` and
`Y` coordinates transports to `c • (κ.withDensity w).prod ν`.

Three ingredients and no analysis: a product of additive Haar measures is additive Haar, the pushforward of an additive Haar measure along a continuous additive equivalence is additive Haar, and two additive Haar measures on the same group differ by a positive finite scalar. Going through the additive equivalence rather than a linear one keeps the statements at the generality of second-countable locally compact additive groups, with no vector-space structure needed. The commutation with a density is stated separately because Mathlib has no lemma commuting a pushforward with withDensity; that gap is filled here.

This is the bookkeeping a Fubini step over the last coordinate of a parameter space needs when the measure is presented abstractly as a Haar measure rather than as a product.

The weighted Sobolev identity in one variable

Theorem5.1.18

uses 1used by 0✓L∃∀N

Smoothness is decay. The L² norm of the k-th derivative of a function on the line is the L² norm of its Fourier transform weighted by the k-th power of the frequency, and the weighted transform is square-integrable exactly when the derivative is.

Lean code for Theorem5.1.18●8 theorems

theoremdefined in LeanRidgelet/ToMathlib/WeightedSobolevOneDim.lean

complete

theorem MeasureTheory.Integrable.eLpNorm_fourier.{u_1, u_2} {F : Type u_1}
  [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
  {E : Type u_2} [NormedAddCommGroup E] [MeasurableSpace E]
  [BorelSpace E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  {f : E → F} (hf : MeasureTheory.Integrable f MeasureTheory.volume)
  (h2 : MeasureTheory.MemLp f 2 MeasureTheory.volume) :
  MeasureTheory.eLpNorm (FourierTransform.fourier f) 2
      MeasureTheory.volume =
    MeasureTheory.eLpNorm f 2 MeasureTheory.volume

theorem MeasureTheory.Integrable.eLpNorm_fourier.{u_1,
    u_2}
  {F : Type u_1} [NormedAddCommGroup F]
  [InnerProductSpace ℂ F]
  [CompleteSpace F] {E : Type u_2}
  [NormedAddCommGroup E]
  [MeasurableSpace E] [BorelSpace E]
  [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] {f : E → F}
  (hf :
    MeasureTheory.Integrable f
      MeasureTheory.volume)
  (h2 :
    MeasureTheory.MemLp f 2
      MeasureTheory.volume) :
  MeasureTheory.eLpNorm
      (FourierTransform.fourier f) 2
      MeasureTheory.volume =
    MeasureTheory.eLpNorm f 2
      MeasureTheory.volume

**Plancherel's theorem on `L¹ ∩ L²`**, `eLpNorm` form: the Fourier integral is an `L²`
isometry on `L¹ ∩ L²`. Restatement of `MeasureTheory.Integrable.lintegral_enorm_fourier_sq`.

theoremdefined in LeanRidgelet/ToMathlib/WeightedSobolevOneDim.lean

complete

theorem MeasureTheory.eLpNorm_iteratedDeriv_eq_eLpNorm_pow_smul_fourier.{u_1}
  {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F]
  [CompleteSpace F] {g : ℝ → F} {N : ℕ∞} {k : ℕ}
  (hg : ContDiff ℝ (↑N) g)
  (hint :
    ∀ (n : ℕ),
      ↑n ≤ N →
        MeasureTheory.Integrable (iteratedDeriv n g)
          MeasureTheory.volume)
  (hk : ↑k ≤ N)
  (hmem :
    MeasureTheory.MemLp (iteratedDeriv k g) 2 MeasureTheory.volume) :
  MeasureTheory.eLpNorm (iteratedDeriv k g) 2 MeasureTheory.volume =
    MeasureTheory.eLpNorm
      (fun ω ↦ (2 * Real.pi * |ω|) ^ k • FourierTransform.fourier g ω) 2
      MeasureTheory.volume

theorem MeasureTheory.eLpNorm_iteratedDeriv_eq_eLpNorm_pow_smul_fourier.{u_1}
  {F : Type u_1} [NormedAddCommGroup F]
  [InnerProductSpace ℂ F]
  [CompleteSpace F] {g : ℝ → F} {N : ℕ∞}
  {k : ℕ} (hg : ContDiff ℝ (↑N) g)
  (hint :
    ∀ (n : ℕ),
      ↑n ≤ N →
        MeasureTheory.Integrable
          (iteratedDeriv n g)
          MeasureTheory.volume)
  (hk : ↑k ≤ N)
  (hmem :
    MeasureTheory.MemLp
      (iteratedDeriv k g) 2
      MeasureTheory.volume) :
  MeasureTheory.eLpNorm
      (iteratedDeriv k g) 2
      MeasureTheory.volume =
    MeasureTheory.eLpNorm
      (fun ω ↦
        (2 * Real.pi * |ω|) ^ k •
          FourierTransform.fourier g ω)
      2 MeasureTheory.volume

**The one-variable weighted Sobolev identity**, Mathlib's `2π` Fourier convention:
`‖g^{(k)}‖_{L²} = ‖(2π|ω|)^k 𝓕 g‖_{L²}`.

The hypotheses are exactly those of `Real.fourier_iteratedDeriv` (`g` is `C^N` and all its
derivatives up to order `N` are integrable, with `k ≤ N`) together with the square-integrability
of `g^{(k)}` needed by Plancherel. The weight `(2π|ω|)^k` is the modulus of the multiplier
`(2πiω)^k` produced by `Real.fourier_iteratedDeriv`.

theoremdefined in LeanRidgelet/ToMathlib/WeightedSobolevOneDim.lean

complete

theorem MeasureTheory.memLp_two_pow_smul_fourier.{u_1} {F : Type u_1}
  [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
  {g : ℝ → F} {N : ℕ∞} {k : ℕ} (hg : ContDiff ℝ (↑N) g)
  (hint :
    ∀ (n : ℕ),
      ↑n ≤ N →
        MeasureTheory.Integrable (iteratedDeriv n g)
          MeasureTheory.volume)
  (hk : ↑k ≤ N)
  (hmem :
    MeasureTheory.MemLp (iteratedDeriv k g) 2 MeasureTheory.volume) :
  MeasureTheory.MemLp
    (fun ω ↦ (2 * Real.pi * |ω|) ^ k • FourierTransform.fourier g ω) 2
    MeasureTheory.volume

theorem MeasureTheory.memLp_two_pow_smul_fourier.{u_1}
  {F : Type u_1} [NormedAddCommGroup F]
  [InnerProductSpace ℂ F]
  [CompleteSpace F] {g : ℝ → F} {N : ℕ∞}
  {k : ℕ} (hg : ContDiff ℝ (↑N) g)
  (hint :
    ∀ (n : ℕ),
      ↑n ≤ N →
        MeasureTheory.Integrable
          (iteratedDeriv n g)
          MeasureTheory.volume)
  (hk : ↑k ≤ N)
  (hmem :
    MeasureTheory.MemLp
      (iteratedDeriv k g) 2
      MeasureTheory.volume) :
  MeasureTheory.MemLp
    (fun ω ↦
      (2 * Real.pi * |ω|) ^ k •
        FourierTransform.fourier g ω)
    2 MeasureTheory.volume

The frequency-weighted Fourier transform of a function whose `k`-th derivative is
square-integrable is itself square-integrable, Mathlib's `2π` convention.

theoremdefined in LeanRidgelet/ToMathlib/WeightedSobolevOneDim.lean

complete

theorem SchwartzMap.iteratedDeriv_eq_iterate_derivCLM.{u_1} {F : Type u_1}
  [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ)
  (g : SchwartzMap ℝ F) :
  iteratedDeriv k ⇑g = ⇑((⇑(SchwartzMap.derivCLM ℝ F))^[k] g)

theorem SchwartzMap.iteratedDeriv_eq_iterate_derivCLM.{u_1}
  {F : Type u_1} [NormedAddCommGroup F]
  [NormedSpace ℝ F] (k : ℕ)
  (g : SchwartzMap ℝ F) :
  iteratedDeriv k ⇑g =
    ⇑((⇑(SchwartzMap.derivCLM ℝ F))^[k] g)

The `k`-th derivative of a Schwartz function on `ℝ` is the `k`-fold iterate of
`SchwartzMap.derivCLM`, in particular again a Schwartz function.

theoremdefined in LeanRidgelet/ToMathlib/WeightedSobolevOneDim.lean

complete

theorem SchwartzMap.integrable_iteratedDeriv.{u_1} {F : Type u_1}
  [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ)
  (g : SchwartzMap ℝ F) :
  MeasureTheory.Integrable (iteratedDeriv k ⇑g) MeasureTheory.volume

theorem SchwartzMap.integrable_iteratedDeriv.{u_1}
  {F : Type u_1} [NormedAddCommGroup F]
  [NormedSpace ℝ F] (k : ℕ)
  (g : SchwartzMap ℝ F) :
  MeasureTheory.Integrable
    (iteratedDeriv k ⇑g)
    MeasureTheory.volume

Every derivative of a Schwartz function on `ℝ` is integrable.

theoremdefined in LeanRidgelet/ToMathlib/WeightedSobolevOneDim.lean

complete

theorem SchwartzMap.memLp_two_iteratedDeriv.{u_1} {F : Type u_1}
  [NormedAddCommGroup F] [NormedSpace ℝ F] (k : ℕ)
  (g : SchwartzMap ℝ F) :
  MeasureTheory.MemLp (iteratedDeriv k ⇑g) 2 MeasureTheory.volume

theorem SchwartzMap.memLp_two_iteratedDeriv.{u_1}
  {F : Type u_1} [NormedAddCommGroup F]
  [NormedSpace ℝ F] (k : ℕ)
  (g : SchwartzMap ℝ F) :
  MeasureTheory.MemLp (iteratedDeriv k ⇑g)
    2 MeasureTheory.volume

Every derivative of a Schwartz function on `ℝ` is square-integrable.

theoremdefined in LeanRidgelet/ToMathlib/WeightedSobolevOneDim.lean

complete

theorem SchwartzMap.eLpNorm_iteratedDeriv_eq_eLpNorm_pow_smul_fourier.{u_1}
  {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℂ F]
  [CompleteSpace F] (k : ℕ) (g : SchwartzMap ℝ F) :
  MeasureTheory.eLpNorm (iteratedDeriv k ⇑g) 2 MeasureTheory.volume =
    MeasureTheory.eLpNorm
      (fun ω ↦
        (2 * Real.pi * |ω|) ^ k • FourierTransform.fourier (⇑g) ω)
      2 MeasureTheory.volume

theorem SchwartzMap.eLpNorm_iteratedDeriv_eq_eLpNorm_pow_smul_fourier.{u_1}
  {F : Type u_1} [NormedAddCommGroup F]
  [InnerProductSpace ℂ F]
  [CompleteSpace F] (k : ℕ)
  (g : SchwartzMap ℝ F) :
  MeasureTheory.eLpNorm
      (iteratedDeriv k ⇑g) 2
      MeasureTheory.volume =
    MeasureTheory.eLpNorm
      (fun ω ↦
        (2 * Real.pi * |ω|) ^ k •
          FourierTransform.fourier (⇑g) ω)
      2 MeasureTheory.volume

**The one-variable weighted Sobolev identity for Schwartz functions**, Mathlib's `2π`
Fourier convention: `‖g^{(k)}‖_{L²} = ‖(2π|ω|)^k 𝓕 g‖_{L²}`. Every hypothesis of
`MeasureTheory.eLpNorm_iteratedDeriv_eq_eLpNorm_pow_smul_fourier` is automatic here.

theoremdefined in LeanRidgelet/ToMathlib/WeightedSobolevOneDim.lean

complete

theorem SchwartzMap.memLp_two_pow_smul_fourier.{u_1} {F : Type u_1}
  [NormedAddCommGroup F] [InnerProductSpace ℂ F] [CompleteSpace F]
  (k : ℕ) (g : SchwartzMap ℝ F) :
  MeasureTheory.MemLp
    (fun ω ↦ (2 * Real.pi * |ω|) ^ k • FourierTransform.fourier (⇑g) ω)
    2 MeasureTheory.volume

theorem SchwartzMap.memLp_two_pow_smul_fourier.{u_1}
  {F : Type u_1} [NormedAddCommGroup F]
  [InnerProductSpace ℂ F]
  [CompleteSpace F] (k : ℕ)
  (g : SchwartzMap ℝ F) :
  MeasureTheory.MemLp
    (fun ω ↦
      (2 * Real.pi * |ω|) ^ k •
        FourierTransform.fourier (⇑g) ω)
    2 MeasureTheory.volume

The frequency-weighted Fourier transform of a Schwartz function on `ℝ` is
square-integrable, Mathlib's `2π` convention.

Two inputs and no analysis of its own: the Fourier transform of an iterated derivative is a power of the frequency times the transform, and Plancherel turns that into an identity of norms. The weight that comes out is the k-th power of 2π times the absolute frequency, the factor being the modulus of the multiplier rather than a choice. For a Schwartz function every hypothesis is automatic, which is the form the application uses; the general form asks for the smoothness and the integrability of the derivatives that the multiplier identity needs.

This is the missing bridge for the boundedness route of the harmonic-analysis track. There a derivative in an additive parameter is moved onto the analysis feature, and the identity converts that into a bound in a frequency-weighted coefficient space — smoothness of the feature and of the data becoming decay of the transform.

Bounded integral operators with a square-integrable kernel

Theorem5.1.19

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 4.5.5

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Hilbert--Schmidt bound. If the kernel k is square-integrable for the product measure, then f\mapsto\int f(y)\overline{k(\cdot,y)}\,dy maps L^2 to L^2 with \|Tf\|_2\le\|k\|_{L^2(\mu\otimes\mu)}\|f\|_2.

Lean code for Theorem5.1.19●22 declarations

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.eLpNorm_rpow_toReal_eq_lintegral.{u_3, u_4} {E : Type u_3}
  [NormedAddCommGroup E] {p : ENNReal} {γ : Type u_4}
  [MeasurableSpace γ] {ρ : MeasureTheory.Measure γ} {g : γ → E}
  (hp0 : p ≠ 0) (hptop : p ≠ ⊤) :
  MeasureTheory.eLpNorm g p ρ ^ p.toReal =
    ∫⁻ (y : γ), ‖g y‖ₑ ^ p.toReal ∂ρ

theorem MeasureTheory.eLpNorm_rpow_toReal_eq_lintegral.{u_3,
    u_4}
  {E : Type u_3} [NormedAddCommGroup E]
  {p : ENNReal} {γ : Type u_4}
  [MeasurableSpace γ]
  {ρ : MeasureTheory.Measure γ}
  {g : γ → E} (hp0 : p ≠ 0)
  (hptop : p ≠ ⊤) :
  MeasureTheory.eLpNorm g p ρ ^ p.toReal =
    ∫⁻ (y : γ), ‖g y‖ₑ ^ p.toReal ∂ρ

For a finite nonzero exponent the `p`-th power of `MeasureTheory.eLpNorm` is the
`ℝ≥0∞`-valued integral of `‖·‖ₑ ^ p`. This is the form in which both sides of Tonelli's theorem are
recognised below.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.lintegral_eLpNorm_rpow_prodMk_left.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β] [NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  {p : ENNReal} [MeasureTheory.SFinite ν] (hp0 : p ≠ 0) (hptop : p ≠ ⊤)
  {k : α × β → E}
  (hk : MeasureTheory.AEStronglyMeasurable k (μ.prod ν)) :
  ∫⁻ (x : α),
      MeasureTheory.eLpNorm (fun y ↦ k (x, y)) p ν ^ p.toReal ∂μ =
    MeasureTheory.eLpNorm k p (μ.prod ν) ^ p.toReal

theorem MeasureTheory.lintegral_eLpNorm_rpow_prodMk_left.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β]
  [NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  {p : ENNReal} [MeasureTheory.SFinite ν]
  (hp0 : p ≠ 0) (hptop : p ≠ ⊤)
  {k : α × β → E}
  (hk :
    MeasureTheory.AEStronglyMeasurable k
      (μ.prod ν)) :
  ∫⁻ (x : α),
      MeasureTheory.eLpNorm
          (fun y ↦ k (x, y)) p ν ^
        p.toReal ∂μ =
    MeasureTheory.eLpNorm k p (μ.prod ν) ^
      p.toReal

Tonelli's theorem in the form used for Hilbert-Schmidt kernels: the `p`-th power of the
`Lᵖ (μ ⊗ ν)` norm of `k` is the integral over `x` of the `p`-th powers of the slice norms
`‖k (x, ·)‖_{Lᵖ(ν)}`. Both sides are the `ℝ≥0∞`-valued integral of `‖k‖ₑ ^ p`, computed either on
the product or as an iterated integral.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.MemLp.prodMk_left.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β]
  [NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {p : ENNReal} [MeasureTheory.SFinite ν]
  {k : α × β → E} (hk : MeasureTheory.MemLp k p (μ.prod ν)) :
  ∀ᵐ (x : α) ∂μ, MeasureTheory.MemLp (fun y ↦ k (x, y)) p ν

theorem MeasureTheory.MemLp.prodMk_left.{u_1, u_2,
    u_3}
  {α : Type u_1} {β : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β]
  [NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  {p : ENNReal} [MeasureTheory.SFinite ν]
  {k : α × β → E}
  (hk :
    MeasureTheory.MemLp k p (μ.prod ν)) :
  ∀ᵐ (x : α) ∂μ,
    MeasureTheory.MemLp (fun y ↦ k (x, y))
      p ν

Almost every slice of an `Lᵖ` function on a product measure is again `Lᵖ`. This is the
`MeasureTheory.MemLp` analogue of `MeasureTheory.Integrable.prod_right_ae`, and the exponent `p` is
arbitrary: for `0 < p < ∞` it follows from Tonelli, for `p = ∞` from the almost-everywhere bound by
the essential supremum, and for `p = 0` it is measurability alone.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.enorm_integral_mul_conj_le.{u_1} {β : Type u_1}
  [MeasurableSpace β] {ν : MeasureTheory.Measure β} {f g : β → ℂ}
  (hf : MeasureTheory.MemLp f 2 ν) (hg : MeasureTheory.MemLp g 2 ν) :
  ‖∫ (y : β), f y * (starRingEnd ℂ) (g y) ∂ν‖ₑ ≤
    MeasureTheory.eLpNorm f 2 ν * MeasureTheory.eLpNorm g 2 ν

theorem MeasureTheory.enorm_integral_mul_conj_le.{u_1}
  {β : Type u_1} [MeasurableSpace β]
  {ν : MeasureTheory.Measure β}
  {f g : β → ℂ}
  (hf : MeasureTheory.MemLp f 2 ν)
  (hg : MeasureTheory.MemLp g 2 ν) :
  ‖∫ (y : β),
        f y * (starRingEnd ℂ) (g y) ∂ν‖ₑ ≤
    MeasureTheory.eLpNorm f 2 ν *
      MeasureTheory.eLpNorm g 2 ν

Cauchy-Schwarz for the sesquilinear pairing of two square-integrable functions: the pairing is
dominated in absolute value by the product of the two `L²` norms. This is Hölder's inequality for
the exponents `2, 2, 1` applied to `y ↦ f y * conj (g y)`, preceded by the triangle inequality for
the Bochner integral.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.integrable_mul_conj.{u_1} {β : Type u_1}
  [MeasurableSpace β] {ν : MeasureTheory.Measure β} {f g : β → ℂ}
  (hf : MeasureTheory.MemLp f 2 ν) (hg : MeasureTheory.MemLp g 2 ν) :
  MeasureTheory.Integrable (fun y ↦ f y * (starRingEnd ℂ) (g y)) ν

theorem MeasureTheory.integrable_mul_conj.{u_1}
  {β : Type u_1} [MeasurableSpace β]
  {ν : MeasureTheory.Measure β}
  {f g : β → ℂ}
  (hf : MeasureTheory.MemLp f 2 ν)
  (hg : MeasureTheory.MemLp g 2 ν) :
  MeasureTheory.Integrable
    (fun y ↦ f y * (starRingEnd ℂ) (g y))
    ν

The product of two square-integrable functions, one of them conjugated, is integrable.
Hölder's inequality for the exponents `2, 2, 1`.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.integrable_mul_conj_kernel_ae.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] {k : α × β → ℂ} {f : β → ℂ}
  (hk : MeasureTheory.MemLp k 2 (μ.prod ν))
  (hf : MeasureTheory.MemLp f 2 ν) :
  ∀ᵐ (x : α) ∂μ,
    MeasureTheory.Integrable (fun y ↦ f y * (starRingEnd ℂ) (k (x, y)))
      ν

theorem MeasureTheory.integrable_mul_conj_kernel_ae.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν]
  {k : α × β → ℂ} {f : β → ℂ}
  (hk :
    MeasureTheory.MemLp k 2 (μ.prod ν))
  (hf : MeasureTheory.MemLp f 2 ν) :
  ∀ᵐ (x : α) ∂μ,
    MeasureTheory.Integrable
      (fun y ↦
        f y * (starRingEnd ℂ) (k (x, y)))
      ν

**Slice integrability.** If the kernel `k` is square integrable for the product measure and `f`
is square integrable, then for almost every `x` the integrand `y ↦ f y * conj (k (x, y))` defining
`T f x` is integrable: almost every slice `k (x, ·)` lies in `L²` by
`MeasureTheory.MemLp.prodMk_left`, and the product of two `L²` functions is `L¹`.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.enorm_integral_mul_conj_kernel_le_ae.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] {k : α × β → ℂ} {f : β → ℂ}
  (hk : MeasureTheory.MemLp k 2 (μ.prod ν))
  (hf : MeasureTheory.MemLp f 2 ν) :
  ∀ᵐ (x : α) ∂μ,
    ‖∫ (y : β), f y * (starRingEnd ℂ) (k (x, y)) ∂ν‖ₑ ≤
      MeasureTheory.eLpNorm f 2 ν *
        MeasureTheory.eLpNorm (fun y ↦ k (x, y)) 2 ν

theorem MeasureTheory.enorm_integral_mul_conj_kernel_le_ae.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν]
  {k : α × β → ℂ} {f : β → ℂ}
  (hk :
    MeasureTheory.MemLp k 2 (μ.prod ν))
  (hf : MeasureTheory.MemLp f 2 ν) :
  ∀ᵐ (x : α) ∂μ,
    ‖∫ (y : β),
          f y *
            (starRingEnd ℂ)
              (k (x, y)) ∂ν‖ₑ ≤
      MeasureTheory.eLpNorm f 2 ν *
        MeasureTheory.eLpNorm
          (fun y ↦ k (x, y)) 2 ν

**Pointwise bound.** For almost every `x` the value `T f x` is bounded by the product of the
`L²` norm of `f` and the `L²` norm of the slice `k (x, ·)`. This is Cauchy-Schwarz on the slice,
available for almost every `x` because almost every slice is square integrable.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.aestronglyMeasurable_integral_mul_conj_kernel.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] {k : α × β → ℂ} {f : β → ℂ}
  (hk : MeasureTheory.MemLp k 2 (μ.prod ν))
  (hf : MeasureTheory.MemLp f 2 ν) :
  MeasureTheory.AEStronglyMeasurable
    (fun x ↦ ∫ (y : β), f y * (starRingEnd ℂ) (k (x, y)) ∂ν) μ

theorem MeasureTheory.aestronglyMeasurable_integral_mul_conj_kernel.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν]
  {k : α × β → ℂ} {f : β → ℂ}
  (hk :
    MeasureTheory.MemLp k 2 (μ.prod ν))
  (hf : MeasureTheory.MemLp f 2 ν) :
  MeasureTheory.AEStronglyMeasurable
    (fun x ↦
      ∫ (y : β),
        f y *
          (starRingEnd ℂ) (k (x, y)) ∂ν)
    μ

Almost everywhere strong measurability of `T f`, from the a.e. strong measurability of the
integrand on the product measure.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.eLpNorm_integral_mul_conj_kernel_le.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] {k : α × β → ℂ} {f : β → ℂ}
  (hk : MeasureTheory.MemLp k 2 (μ.prod ν))
  (hf : MeasureTheory.MemLp f 2 ν) :
  MeasureTheory.eLpNorm
      (fun x ↦ ∫ (y : β), f y * (starRingEnd ℂ) (k (x, y)) ∂ν) 2 μ ≤
    MeasureTheory.eLpNorm k 2 (μ.prod ν) * MeasureTheory.eLpNorm f 2 ν

theorem MeasureTheory.eLpNorm_integral_mul_conj_kernel_le.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν]
  {k : α × β → ℂ} {f : β → ℂ}
  (hk :
    MeasureTheory.MemLp k 2 (μ.prod ν))
  (hf : MeasureTheory.MemLp f 2 ν) :
  MeasureTheory.eLpNorm
      (fun x ↦
        ∫ (y : β),
          f y *
            (starRingEnd ℂ) (k (x, y)) ∂ν)
      2 μ ≤
    MeasureTheory.eLpNorm k 2 (μ.prod ν) *
      MeasureTheory.eLpNorm f 2 ν

**The main estimate.** The operator `T` with square-integrable kernel `k` maps `L² ν` into
`L² μ` with `‖T f‖_{L²(μ)} ≤ ‖k‖_{L²(μ ⊗ ν)} * ‖f‖_{L²(ν)}`. The pointwise Cauchy-Schwarz bound is
squared and integrated in `x`, and Tonelli reassembles the squared slice norms into the
product-measure norm of `k`.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.memLp_integral_mul_conj_kernel.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] {k : α × β → ℂ} {f : β → ℂ}
  (hk : MeasureTheory.MemLp k 2 (μ.prod ν))
  (hf : MeasureTheory.MemLp f 2 ν) :
  MeasureTheory.MemLp
    (fun x ↦ ∫ (y : β), f y * (starRingEnd ℂ) (k (x, y)) ∂ν) 2 μ

theorem MeasureTheory.memLp_integral_mul_conj_kernel.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν]
  {k : α × β → ℂ} {f : β → ℂ}
  (hk :
    MeasureTheory.MemLp k 2 (μ.prod ν))
  (hf : MeasureTheory.MemLp f 2 ν) :
  MeasureTheory.MemLp
    (fun x ↦
      ∫ (y : β),
        f y *
          (starRingEnd ℂ) (k (x, y)) ∂ν)
    2 μ

**The main estimate, membership half.** With a square-integrable kernel, `T f` is again square
integrable whenever `f` is.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.eLpNorm_prod_swap.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β]
  [NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] {p : ENNReal} {k : α × β → E}
  (hk : MeasureTheory.AEStronglyMeasurable k (μ.prod ν)) :
  MeasureTheory.eLpNorm (fun z ↦ k z.swap) p (ν.prod μ) =
    MeasureTheory.eLpNorm k p (μ.prod ν)

theorem MeasureTheory.eLpNorm_prod_swap.{u_1, u_2,
    u_3}
  {α : Type u_1} {β : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β]
  [NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] {p : ENNReal}
  {k : α × β → E}
  (hk :
    MeasureTheory.AEStronglyMeasurable k
      (μ.prod ν)) :
  MeasureTheory.eLpNorm (fun z ↦ k z.swap)
      p (ν.prod μ) =
    MeasureTheory.eLpNorm k p (μ.prod ν)

Exchanging the two arguments of a kernel leaves its `Lᵖ` norm unchanged, because
`Prod.swap` is measure preserving from `ν ⊗ μ` to `μ ⊗ ν`.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.MemLp.prod_swap.{u_1, u_2, u_3} {α : Type u_1}
  {β : Type u_2} {E : Type u_3} [MeasurableSpace α] [MeasurableSpace β]
  [NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] {p : ENNReal} {k : α × β → E}
  (hk : MeasureTheory.MemLp k p (μ.prod ν)) :
  MeasureTheory.MemLp (fun z ↦ k z.swap) p (ν.prod μ)

theorem MeasureTheory.MemLp.prod_swap.{u_1, u_2,
    u_3}
  {α : Type u_1} {β : Type u_2}
  {E : Type u_3} [MeasurableSpace α]
  [MeasurableSpace β]
  [NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν] {p : ENNReal}
  {k : α × β → E}
  (hk :
    MeasureTheory.MemLp k p (μ.prod ν)) :
  MeasureTheory.MemLp (fun z ↦ k z.swap) p
    (ν.prod μ)

Exchanging the two arguments of an `Lᵖ` kernel gives an `Lᵖ` kernel for the exchanged product
measure. This is `MeasureTheory.AEMeasurable.prod_swap` for `MeasureTheory.MemLp`.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.eLpNorm_integral_feature_analysis_le.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {ψ : α × β → ℂ}
  {f : α → ℂ} (hψ : MeasureTheory.MemLp ψ 2 (μ.prod ν))
  (hf : MeasureTheory.MemLp f 2 μ) :
  MeasureTheory.eLpNorm
      (fun ξ ↦ ∫ (y : α), f y * (starRingEnd ℂ) (ψ (y, ξ)) ∂μ) 2 ν ≤
    MeasureTheory.eLpNorm ψ 2 (μ.prod ν) * MeasureTheory.eLpNorm f 2 μ

theorem MeasureTheory.eLpNorm_integral_feature_analysis_le.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  {ψ : α × β → ℂ} {f : α → ℂ}
  (hψ :
    MeasureTheory.MemLp ψ 2 (μ.prod ν))
  (hf : MeasureTheory.MemLp f 2 μ) :
  MeasureTheory.eLpNorm
      (fun ξ ↦
        ∫ (y : α),
          f y *
            (starRingEnd ℂ) (ψ (y, ξ)) ∂μ)
      2 ν ≤
    MeasureTheory.eLpNorm ψ 2 (μ.prod ν) *
      MeasureTheory.eLpNorm f 2 μ

**The ridgelet transform is bounded.** As an operator from the data space `(α, μ)` to the
parameter space `(β, ν)`, the transform against `ψ` has kernel `ψ` with its two arguments
exchanged, so the Hilbert-Schmidt estimate applies and `MeasureTheory.eLpNorm_prod_swap` restores
the original order in the bound.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.memLp_integral_feature_analysis.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {ψ : α × β → ℂ}
  {f : α → ℂ} (hψ : MeasureTheory.MemLp ψ 2 (μ.prod ν))
  (hf : MeasureTheory.MemLp f 2 μ) :
  MeasureTheory.MemLp
    (fun ξ ↦ ∫ (y : α), f y * (starRingEnd ℂ) (ψ (y, ξ)) ∂μ) 2 ν

theorem MeasureTheory.memLp_integral_feature_analysis.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  {ψ : α × β → ℂ} {f : α → ℂ}
  (hψ :
    MeasureTheory.MemLp ψ 2 (μ.prod ν))
  (hf : MeasureTheory.MemLp f 2 μ) :
  MeasureTheory.MemLp
    (fun ξ ↦
      ∫ (y : α),
        f y *
          (starRingEnd ℂ) (ψ (y, ξ)) ∂μ)
    2 ν

**The ridgelet transform is bounded, membership half.** The transform of a square-integrable
function against a square-integrable feature map is square integrable on the parameter space.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.eLpNorm_integral_feature_composite_le.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {φ ψ : α × β → ℂ}
  {f : α → ℂ} (hφ : MeasureTheory.MemLp φ 2 (μ.prod ν))
  (hψ : MeasureTheory.MemLp ψ 2 (μ.prod ν))
  (hf : MeasureTheory.MemLp f 2 μ) :
  MeasureTheory.eLpNorm
      (fun x ↦
        ∫ (ξ : β),
          (∫ (y : α), f y * (starRingEnd ℂ) (ψ (y, ξ)) ∂μ) *
            (starRingEnd ℂ) (φ (x, ξ)) ∂ν)
      2 μ ≤
    MeasureTheory.eLpNorm φ 2 (μ.prod ν) *
        MeasureTheory.eLpNorm ψ 2 (μ.prod ν) *
      MeasureTheory.eLpNorm f 2 μ

theorem MeasureTheory.eLpNorm_integral_feature_composite_le.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  {φ ψ : α × β → ℂ} {f : α → ℂ}
  (hφ :
    MeasureTheory.MemLp φ 2 (μ.prod ν))
  (hψ :
    MeasureTheory.MemLp ψ 2 (μ.prod ν))
  (hf : MeasureTheory.MemLp f 2 μ) :
  MeasureTheory.eLpNorm
      (fun x ↦
        ∫ (ξ : β),
          (∫ (y : α),
              f y *
                (starRingEnd ℂ)
                  (ψ (y, ξ)) ∂μ) *
            (starRingEnd ℂ) (φ (x, ξ)) ∂ν)
      2 μ ≤
    MeasureTheory.eLpNorm φ 2 (μ.prod ν) *
        MeasureTheory.eLpNorm ψ 2
          (μ.prod ν) *
      MeasureTheory.eLpNorm f 2 μ

**Condition T2.** If both feature maps are square integrable for `μ ⊗ ν`, then the composite of
the ridgelet transform against `ψ` and the synthesis against `φ` is bounded on `L² μ`, with
`‖T f‖_{L²(μ)} ≤ ‖φ‖_{L²(μ ⊗ ν)} * ‖ψ‖_{L²(μ ⊗ ν)} * ‖f‖_{L²(μ)}`. Both halves are instances of
`MeasureTheory.eLpNorm_integral_mul_conj_kernel_le`, the analysis with kernel `ψ` from `(α, μ)` to
`(β, ν)`, the synthesis with kernel `φ` from `(β, ν)` back to `(α, μ)`.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.memLp_integral_feature_composite.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {φ ψ : α × β → ℂ}
  {f : α → ℂ} (hφ : MeasureTheory.MemLp φ 2 (μ.prod ν))
  (hψ : MeasureTheory.MemLp ψ 2 (μ.prod ν))
  (hf : MeasureTheory.MemLp f 2 μ) :
  MeasureTheory.MemLp
    (fun x ↦
      ∫ (ξ : β),
        (∫ (y : α), f y * (starRingEnd ℂ) (ψ (y, ξ)) ∂μ) *
          (starRingEnd ℂ) (φ (x, ξ)) ∂ν)
    2 μ

theorem MeasureTheory.memLp_integral_feature_composite.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  {φ ψ : α × β → ℂ} {f : α → ℂ}
  (hφ :
    MeasureTheory.MemLp φ 2 (μ.prod ν))
  (hψ :
    MeasureTheory.MemLp ψ 2 (μ.prod ν))
  (hf : MeasureTheory.MemLp f 2 μ) :
  MeasureTheory.MemLp
    (fun x ↦
      ∫ (ξ : β),
        (∫ (y : α),
            f y *
              (starRingEnd ℂ)
                (ψ (y, ξ)) ∂μ) *
          (starRingEnd ℂ) (φ (x, ξ)) ∂ν)
    2 μ

**Condition T2, membership half.** With two square-integrable feature maps the composite of the
ridgelet transform and the synthesis maps `L² μ` into itself.

defdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

def MeasureTheory.hilbertSchmidtKernelLinearMap.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] {k : α × β → ℂ}
  (hk : MeasureTheory.MemLp k 2 (μ.prod ν)) :
  ↥(MeasureTheory.Lp ℂ 2 ν) →ₗ[ℂ] ↥(MeasureTheory.Lp ℂ 2 μ)

def MeasureTheory.hilbertSchmidtKernelLinearMap.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν]
  {k : α × β → ℂ}
  (hk :
    MeasureTheory.MemLp k 2 (μ.prod ν)) :
  ↥(MeasureTheory.Lp ℂ 2 ν) →ₗ[ℂ]
    ↥(MeasureTheory.Lp ℂ 2 μ)

Implementation after :=

:= (memLp_integral_mul_conj_kernel hk (Lp.memLp f)).toLp _
  map_add' f g := by
    refine Lp.ext_iff.2 ?_
    filter_upwards [MemLp.coeFn_toLp (memLp_integral_mul_conj_kernel hk (Lp.memLp (f + g))),
      Lp.coeFn_add ((memLp_integral_mul_conj_kernel hk (Lp.memLp f)).toLp _)
        ((memLp_integral_mul_conj_kernel hk (Lp.memLp g)).toLp _),
      MemLp.coeFn_toLp (memLp_integral_mul_conj_kernel hk (Lp.memLp f)),
      MemLp.coeFn_toLp (memLp_integral_mul_conj_kernel hk (Lp.memLp g)),
      integrable_mul_conj_kernel_ae hk (Lp.memLp f),
      integrable_mul_conj_kernel_ae hk (Lp.memLp g)] with x h1 h2 h3 h4 hif hig
    have hsplit : ∫ y, (↑↑(f + g) : β → ℂ) y * conj (k (x, y)) ∂ν =
        ∫ y, ((↑↑f : β → ℂ) y * conj (k (x, y)) +
          (↑↑g : β → ℂ) y * conj (k (x, y))) ∂ν := by
      refine integral_congr_ae ?_
      filter_upwards [Lp.coeFn_add f g] with y hy
      rw [hy]
      simp [add_mul]
    rw [h1, h2, Pi.add_apply, h3, h4, hsplit, integral_add hif hig]
  map_smul' c f := by
    refine Lp.ext_iff.2 ?_
    filter_upwards [MemLp.coeFn_toLp (memLp_integral_mul_conj_kernel hk (Lp.memLp (c • f))),
      Lp.coeFn_smul c ((memLp_integral_mul_conj_kernel hk (Lp.memLp f)).toLp _),
      MemLp.coeFn_toLp (memLp_integral_mul_conj_kernel hk (Lp.memLp f))] with x h1 h2 h3
    have hsmul : ∫ y, (↑↑(c • f) : β → ℂ) y * conj (k (x, y)) ∂ν =
        c * ∫ y, (↑↑f : β → ℂ) y * conj (k (x, y)) ∂ν := by
      rw [← integral_const_mul]
      refine integral_congr_ae ?_
      filter_upwards [Lp.coeFn_smul c f] with y hy
      rw [hy]
      simp [mul_assoc]
    simp only [RingHom.id_apply]
    rw [h1, h2, Pi.smul_apply, h3, smul_eq_mul, hsmul]

The integral operator of a square-integrable kernel, as a linear map between the scalar `L²`
spaces.  The image lies in `L²` by `MeasureTheory.memLp_integral_mul_conj_kernel`, and additivity
uses the almost-everywhere slice integrability that lets the integral be split.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.coeFn_hilbertSchmidtKernelLinearMap.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] {k : α × β → ℂ}
  (hk : MeasureTheory.MemLp k 2 (μ.prod ν))
  (f : ↥(MeasureTheory.Lp ℂ 2 ν)) :
  ↑↑((MeasureTheory.hilbertSchmidtKernelLinearMap hk) f) =ᵐ[μ] fun x ↦
    ∫ (y : β), ↑↑f y * (starRingEnd ℂ) (k (x, y)) ∂ν

theorem MeasureTheory.coeFn_hilbertSchmidtKernelLinearMap.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν]
  {k : α × β → ℂ}
  (hk :
    MeasureTheory.MemLp k 2 (μ.prod ν))
  (f : ↥(MeasureTheory.Lp ℂ 2 ν)) :
  ↑↑((MeasureTheory.hilbertSchmidtKernelLinearMap
            hk)
          f) =ᵐ[μ]
    fun x ↦
    ∫ (y : β),
      ↑↑f y *
        (starRingEnd ℂ) (k (x, y)) ∂ν

The representative of the operator's value is the pointwise integral.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.norm_hilbertSchmidtKernelLinearMap_le.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] {k : α × β → ℂ}
  (hk : MeasureTheory.MemLp k 2 (μ.prod ν))
  (f : ↥(MeasureTheory.Lp ℂ 2 ν)) :
  ‖(MeasureTheory.hilbertSchmidtKernelLinearMap hk) f‖ ≤
    (MeasureTheory.eLpNorm k 2 (μ.prod ν)).toReal * ‖f‖

theorem MeasureTheory.norm_hilbertSchmidtKernelLinearMap_le.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν]
  {k : α × β → ℂ}
  (hk :
    MeasureTheory.MemLp k 2 (μ.prod ν))
  (f : ↥(MeasureTheory.Lp ℂ 2 ν)) :
  ‖(MeasureTheory.hilbertSchmidtKernelLinearMap
          hk)
        f‖ ≤
    (MeasureTheory.eLpNorm k 2
          (μ.prod ν)).toReal *
      ‖f‖

The value of the operator has norm at most the `L²` norm of the kernel times the norm of the
input.

defdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

def MeasureTheory.hilbertSchmidtKernelOperator.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] {k : α × β → ℂ}
  (hk : MeasureTheory.MemLp k 2 (μ.prod ν)) :
  ↥(MeasureTheory.Lp ℂ 2 ν) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 μ)

def MeasureTheory.hilbertSchmidtKernelOperator.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν]
  {k : α × β → ℂ}
  (hk :
    MeasureTheory.MemLp k 2 (μ.prod ν)) :
  ↥(MeasureTheory.Lp ℂ 2 ν) →L[ℂ]
    ↥(MeasureTheory.Lp ℂ 2 μ)

Implementation after :=

:=
  LinearMap.mkContinuous (hilbertSchmidtKernelLinearMap hk) (eLpNorm k 2 (μ.prod ν)).toReal
    (norm_hilbertSchmidtKernelLinearMap_le hk)

**Hilbert--Schmidt integral operators are bounded.**  A square-integrable kernel defines a
continuous linear map between the scalar `L²` spaces, of norm at most the `L²` norm of the kernel.
This is the bundled form of condition T1 of the article's boundedness appendix, and it is what
supplies a bounded machine or ridgelet transform to the reconstruction argument.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.coeFn_hilbertSchmidtKernelOperator.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] {k : α × β → ℂ}
  (hk : MeasureTheory.MemLp k 2 (μ.prod ν))
  (f : ↥(MeasureTheory.Lp ℂ 2 ν)) :
  ↑↑((MeasureTheory.hilbertSchmidtKernelOperator hk) f) =ᵐ[μ] fun x ↦
    ∫ (y : β), ↑↑f y * (starRingEnd ℂ) (k (x, y)) ∂ν

theorem MeasureTheory.coeFn_hilbertSchmidtKernelOperator.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν]
  {k : α × β → ℂ}
  (hk :
    MeasureTheory.MemLp k 2 (μ.prod ν))
  (f : ↥(MeasureTheory.Lp ℂ 2 ν)) :
  ↑↑((MeasureTheory.hilbertSchmidtKernelOperator
            hk)
          f) =ᵐ[μ]
    fun x ↦
    ∫ (y : β),
      ↑↑f y *
        (starRingEnd ℂ) (k (x, y)) ∂ν

The representative of the bundled operator's value is the pointwise integral.

theoremdefined in LeanRidgelet/ToMathlib/HilbertSchmidtKernel.lean

complete

theorem MeasureTheory.norm_hilbertSchmidtKernelOperator_le.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] {k : α × β → ℂ}
  (hk : MeasureTheory.MemLp k 2 (μ.prod ν)) :
  ‖MeasureTheory.hilbertSchmidtKernelOperator hk‖ ≤
    (MeasureTheory.eLpNorm k 2 (μ.prod ν)).toReal

theorem MeasureTheory.norm_hilbertSchmidtKernelOperator_le.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [MeasurableSpace α] [MeasurableSpace β]
  {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν]
  {k : α × β → ℂ}
  (hk :
    MeasureTheory.MemLp k 2 (μ.prod ν)) :
  ‖MeasureTheory.hilbertSchmidtKernelOperator
        hk‖ ≤
    (MeasureTheory.eLpNorm k 2
        (μ.prod ν)).toReal

The operator norm of a Hilbert--Schmidt integral operator is at most the `L²` norm of its
kernel.

Almost every slice of a square-integrable kernel is square-integrable — a MemLp slice lemma for product measures that Mathlib does not have, proved here for every exponent by Tonelli below infinity and by the essential-supremum bound at infinity. On such a slice, Cauchy--Schwarz makes the integrand integrable and bounds the integral by the product of the two L² norms; squaring that bound and integrating in the outer variable turns the slice norms back into the product-measure norm, again by Tonelli. The statement is left unbundled: the operator appears as the explicit integral rather than as a continuous linear map, so nothing has to be unfolded at the point of use. This is condition T1 of the article's boundedness appendix.

The kernel need not join a space to itself: the statement is proved between two measure spaces, which is what it was really proving all along, and only the measure integrated against has to be s-finite. Condition T2 of the same appendix follows by using it twice. The analysis map with feature \psi is the kernel operator from the data space to the parameter space, its kernel being the swap of \psi, and the synthesis map with feature \varphi is the kernel operator back; composing the two bounds gives the composite bound with the product of the two feature norms. Making the analysis half a literal instance needs MemLp to be stable under swapping the factors of a product measure, which Mathlib has only for measurability, so that is proved here too. The conjugate is placed on the feature map in the synthesis so that the instance is literal rather than up to a rewrite; the unconjugated reading is the same statement for the conjugate feature, which has the same norm.

The estimate is bundled as well, into a continuous linear map between the two scalar L² spaces whose operator norm is at most the L² norm of the kernel. Additivity is where the slice integrability is needed: splitting the integral of a sum requires each half to be integrable, which holds for almost every point of the outer variable, and that is exactly the almost-everywhere statement proved above. The bundled operator is what a reconstruction argument consumes, since the machine and the ridgelet transform there are bounded operators on L² and not merely pointwise integrals.

Finite-sum discretization of a Bochner integral

Theorem5.1.20

uses 1used by 1✓L∃∀N

Uniform approximation by finite sums. A Lipschitz Banach-valued function on a compact metric space with a finite measure has a Bochner integral, and that integral is approximated in norm, to any accuracy, by finite sums \sum_i w_i\varphi(\xi_i) with nonnegative weights.

Lean code for Theorem5.1.20●4 theorems

theoremdefined in LeanRidgelet/ToMathlib/LipschitzDiscretization.lean

complete

theorem MeasureTheory.exists_fin_measurable_partition_subset_ball.{u_1}
  (Ξ : Type u_1) [MetricSpace Ξ] [CompactSpace Ξ] [MeasurableSpace Ξ]
  [BorelSpace Ξ] {δ : ℝ} (hδ : 0 < δ) :
  ∃ n c S,
    (∀ (i : Fin n), MeasurableSet (S i)) ∧
      (∀ (i : Fin n), S i ⊆ Metric.ball (c i) δ) ∧
        Pairwise (Function.onFun Disjoint S) ∧ ∀ (x : Ξ), ∃ i, x ∈ S i

theorem MeasureTheory.exists_fin_measurable_partition_subset_ball.{u_1}
  (Ξ : Type u_1) [MetricSpace Ξ]
  [CompactSpace Ξ] [MeasurableSpace Ξ]
  [BorelSpace Ξ] {δ : ℝ} (hδ : 0 < δ) :
  ∃ n c S,
    (∀ (i : Fin n), MeasurableSet (S i)) ∧
      (∀ (i : Fin n),
          S i ⊆ Metric.ball (c i) δ) ∧
        Pairwise
            (Function.onFun Disjoint S) ∧
          ∀ (x : Ξ), ∃ i, x ∈ S i

A compact metric space is a finite disjoint union of measurable pieces of small diameter:
for `δ > 0` there are finitely many points `c i` and pairwise disjoint measurable sets `S i`
covering the space with `S i ⊆ ball (c i) δ`. The sets are obtained by making a finite cover by
`δ`-balls disjoint with `disjointed`.

theoremdefined in LeanRidgelet/ToMathlib/LipschitzDiscretization.lean

complete

theorem MeasureTheory.integrable_of_lipschitzWith.{u_1, u_2} {Ξ : Type u_1}
  {F : Type u_2} [MetricSpace Ξ] [CompactSpace Ξ] [MeasurableSpace Ξ]
  [BorelSpace Ξ] [NormedAddCommGroup F] (μ : MeasureTheory.Measure Ξ)
  [MeasureTheory.IsFiniteMeasure μ] {L : NNReal} {φ : Ξ → F}
  (hφ : LipschitzWith L φ) : MeasureTheory.Integrable φ μ

theorem MeasureTheory.integrable_of_lipschitzWith.{u_1,
    u_2}
  {Ξ : Type u_1} {F : Type u_2}
  [MetricSpace Ξ] [CompactSpace Ξ]
  [MeasurableSpace Ξ] [BorelSpace Ξ]
  [NormedAddCommGroup F]
  (μ : MeasureTheory.Measure Ξ)
  [MeasureTheory.IsFiniteMeasure μ]
  {L : NNReal} {φ : Ξ → F}
  (hφ : LipschitzWith L φ) :
  MeasureTheory.Integrable φ μ

A Lipschitz map from a compact metric space to a Banach space is Bochner integrable with
respect to any finite Borel measure: it is continuous, hence measurable and bounded, and a bounded
function is integrable for a finite measure.

theoremdefined in LeanRidgelet/ToMathlib/LipschitzDiscretization.lean

complete

theorem MeasureTheory.exists_finsetSum_approx_integral_of_lipschitz.{u_1, u_2}
  {Ξ : Type u_1} {F : Type u_2} [MetricSpace Ξ] [CompactSpace Ξ]
  [MeasurableSpace Ξ] [BorelSpace Ξ] [NormedAddCommGroup F]
  [NormedSpace ℝ F] [CompleteSpace F] (μ : MeasureTheory.Measure Ξ)
  [MeasureTheory.IsFiniteMeasure μ] {L : NNReal} {φ : Ξ → F}
  (hφ : LipschitzWith L φ) {ε : ℝ} (hε : 0 < ε) :
  ∃ n w ξ,
    (∀ (i : Fin n), 0 ≤ w i) ∧
      ‖∫ (x : Ξ), φ x ∂μ - ∑ i, w i • φ (ξ i)‖ < ε

theorem MeasureTheory.exists_finsetSum_approx_integral_of_lipschitz.{u_1,
    u_2}
  {Ξ : Type u_1} {F : Type u_2}
  [MetricSpace Ξ] [CompactSpace Ξ]
  [MeasurableSpace Ξ] [BorelSpace Ξ]
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  [CompleteSpace F]
  (μ : MeasureTheory.Measure Ξ)
  [MeasureTheory.IsFiniteMeasure μ]
  {L : NNReal} {φ : Ξ → F}
  (hφ : LipschitzWith L φ) {ε : ℝ}
  (hε : 0 < ε) :
  ∃ n w ξ,
    (∀ (i : Fin n), 0 ≤ w i) ∧
      ‖∫ (x : Ξ), φ x ∂μ -
            ∑ i, w i • φ (ξ i)‖ <
        ε

**Discretization of a Bochner integral of a Lipschitz family.** For a Lipschitz map `φ` from a
compact metric space with a finite Borel measure `μ` to a Banach space, the integral `∫ φ ∂μ` is
approximated in norm, to any accuracy `ε > 0`, by a finite sum `∑ i, w i • φ (ξ i)` of point
evaluations with nonnegative weights. The weights are the measures of the pieces of a partition
into sets of radius `δ`, with `δ` chosen so that `L * δ * μ.real univ < ε`, and the points are the
centres of those pieces.

theoremdefined in LeanRidgelet/ToMathlib/LipschitzDiscretization.lean

complete

theorem MeasureTheory.exists_finsetSum_approx_integral_boundedContinuous_of_lipschitz.{u_1,
    u_2, u_3}
  {Ξ : Type u_1} {X : Type u_2} {Y : Type u_3} [MetricSpace Ξ]
  [CompactSpace Ξ] [MeasurableSpace Ξ] [BorelSpace Ξ]
  [TopologicalSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y]
  [CompleteSpace Y] (μ : MeasureTheory.Measure Ξ)
  [MeasureTheory.IsFiniteMeasure μ] {L : NNReal}
  {φ : Ξ → BoundedContinuousFunction X Y} (hφ : LipschitzWith L φ)
  {ε : ℝ} (hε : 0 < ε) :
  ∃ n w ξ,
    (∀ (i : Fin n), 0 ≤ w i) ∧
      ‖∫ (t : Ξ), φ t ∂μ - ∑ i, w i • φ (ξ i)‖ < ε ∧
        ∀ (x : X), ‖(∫ (t : Ξ), φ t ∂μ) x - ∑ i, w i • (φ (ξ i)) x‖ < ε

theorem MeasureTheory.exists_finsetSum_approx_integral_boundedContinuous_of_lipschitz.{u_1,
    u_2, u_3}
  {Ξ : Type u_1} {X : Type u_2}
  {Y : Type u_3} [MetricSpace Ξ]
  [CompactSpace Ξ] [MeasurableSpace Ξ]
  [BorelSpace Ξ] [TopologicalSpace X]
  [NormedAddCommGroup Y] [NormedSpace ℝ Y]
  [CompleteSpace Y]
  (μ : MeasureTheory.Measure Ξ)
  [MeasureTheory.IsFiniteMeasure μ]
  {L : NNReal}
  {φ : Ξ → BoundedContinuousFunction X Y}
  (hφ : LipschitzWith L φ) {ε : ℝ}
  (hε : 0 < ε) :
  ∃ n w ξ,
    (∀ (i : Fin n), 0 ≤ w i) ∧
      ‖∫ (t : Ξ), φ t ∂μ -
              ∑ i, w i • φ (ξ i)‖ <
          ε ∧
        ∀ (x : X),
          ‖(∫ (t : Ξ), φ t ∂μ) x -
                ∑ i, w i • (φ (ξ i)) x‖ <
            ε

**Uniform approximation of a bounded-continuous integral representation by finite sums.** The
case `F := X →ᵇ Y` of `MeasureTheory.exists_finsetSum_approx_integral_of_lipschitz`. Since the
norm of `X →ᵇ Y` is the supremum norm, the estimate is uniform in `x : X`, as the last conjunct
spells out; neither a measure nor compactness is assumed on `X`.

Compactness supplies a finite cover by balls of a chosen radius; disjointifying it gives a finite measurable partition, and the simple function taking the value of the integrand at the centre of each piece is within the Lipschitz constant times that radius of the integrand everywhere. Its integral is exactly the finite sum with weights the measures of the pieces, and the finiteness of the measure turns the pointwise bound into a bound on the difference of the integrals. Taking the value at the centre rather than at an arbitrary point of each piece halves the constant and removes the need to choose representatives, so the empty parameter space needs no separate treatment. Specializing the Banach space to the bounded continuous functions on an arbitrary topological space gives the article's uniform approximation of an integral representation by finite networks: no measure, compactness, or metric on the data space is involved.

Pushing a compactly restricted Haar measure by a surjective linear map

Theorem5.1.21

uses 1used by 1✓L∃∀N

Compactly restricted pushforward bound. Mathlib's LinearMap.exists_map_addHaar_eq_smul_addHaar' pushes a whole additive Haar measure forward along a surjective linear map, and its proportionality factor is infinite as soon as the map has a nontrivial kernel, since the fibers are unbounded. Restricting the source measure to a compact set removes the divergence: the image measure is dominated by a finite multiple of additive Haar measure of the target.

Lean code for Theorem5.1.21●2 theorems

theoremdefined in LeanRidgelet/ToMathlib/LinearSurjectionHaar.lean

complete

theorem MeasureTheory.map_snd_restrict_prod_le.{u_1, u_2} {X : Type u_1}
  {Y : Type u_2} [MeasurableSpace X] [MeasurableSpace Y]
  (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y)
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν]
  (K : Set (X × Y)) :
  MeasureTheory.Measure.map Prod.snd ((μ.prod ν).restrict K) ≤
    μ (Prod.fst '' K) • ν.restrict (Prod.snd '' K)

theorem MeasureTheory.map_snd_restrict_prod_le.{u_1,
    u_2}
  {X : Type u_1} {Y : Type u_2}
  [MeasurableSpace X] [MeasurableSpace Y]
  (μ : MeasureTheory.Measure X)
  (ν : MeasureTheory.Measure Y)
  [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν]
  (K : Set (X × Y)) :
  MeasureTheory.Measure.map Prod.snd
      ((μ.prod ν).restrict K) ≤
    μ (Prod.fst '' K) •
      ν.restrict (Prod.snd '' K)

The image of a restricted product measure under the second projection is dominated by the second
factor, with the measure of the first projection of the restriction set as constant.

theoremdefined in LeanRidgelet/ToMathlib/LinearSurjectionHaar.lean

complete

theorem LinearMap.exists_map_restrict_addHaar_le_smul_addHaar.{u_1, u_2}
  {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F]
  [BorelSpace F] [FiniteDimensional ℝ F] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure] (ν : MeasureTheory.Measure F)
  [ν.IsAddHaarMeasure] {L : E →ₗ[ℝ] F} (hL : Function.Surjective ⇑L)
  {K : Set E} (hK : IsCompact K) :
  ∃ C,
    C ≠ ⊤ ∧
      MeasureTheory.Measure.map (⇑L) (μ.restrict K) ≤
        C • ν.restrict (⇑L '' K)

theorem LinearMap.exists_map_restrict_addHaar_le_smul_addHaar.{u_1,
    u_2}
  {E : Type u_1} {F : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  [MeasurableSpace F] [BorelSpace F]
  [FiniteDimensional ℝ F]
  (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure]
  (ν : MeasureTheory.Measure F)
  [ν.IsAddHaarMeasure] {L : E →ₗ[ℝ] F}
  (hL : Function.Surjective ⇑L)
  {K : Set E} (hK : IsCompact K) :
  ∃ C,
    C ≠ ⊤ ∧
      MeasureTheory.Measure.map (⇑L)
          (μ.restrict K) ≤
        C • ν.restrict (⇑L '' K)

The image under a surjective linear map of an additive Haar measure restricted to a compact set
is dominated by a finite multiple of additive Haar measure on the target.

The proof follows the decomposition used by `LinearMap.exists_map_addHaar_eq_smul_addHaar'`: a
complement `T` of the kernel `S` splits the source as `S × T`, the map becomes the second
projection followed by a linear equivalence, and the compact restriction set has a bounded
kernel projection.

The proof reuses Mathlib's decomposition. A complement T of the kernel S splits the source as S\times T, so the map is the second projection followed by a linear equivalence, and Haar uniqueness turns both the source measure and the target measure into multiples of the corresponding product and pushforward measures. The remaining estimate is elementary and is isolated as its own lemma: the second projection of a product measure restricted to a set is dominated by the second factor, with the measure of the first projection of that set as the constant — finite exactly because the restriction set is compact.