MATHLIBANNEX / CANONICAL DECLARATION CARD

Determinant integrals under strong convergence

MathlibAnnex.MeasureTheory.tendsto_integral_det_of_strongLn

theorem

Uses Hölder’s inequality to turn strong convergence of matrix fields into convergence of their determinant integrals.

Statement

Let , let be a measure space, and let be any filter on an index set . Let , equipped with the operator norm induced by on . Suppose , eventually along , and Then along the same filter.

Assumptions

The dimension is positive. Membership in includes almost-everywhere strong measurability and finite seminorm. The measure need not be finite, and the filter need not be a sequence filter. No pointwise convergence or common pointwise bound is assumed.

Conclusion

The limiting determinant is integrable, the approximating determinants are eventually integrable, and their integrals converge. In fact their differences converge to zero in .

The supplied convergence predicate records both seminorm convergence and eventual membership; the separate hypothesis on is also necessary for the proof. The one-dimensional case is handled directly, without using the undefined exponent at .

Proof route

Apply the determinant difference estimate, then Hölder with exponents and . The resulting bound contains the factor , which tends to zero; the other factor stays bounded by the triangle inequality. Treat directly.

Proof steps

  1. Start with the pointwise estimate and integrability. The determinant bound gives, at every ,

    For any field , comparison with the zero operator gives

    Continuity of determinant supplies measurability, so is integrable. Apply this to and, eventually, to . Hence the determinant difference is eventually integrable. All following estimates are on this eventual set of indices.

  2. If , no nontrivial Hölder exponent is needed. Step 1 reduces to

  3. If , write Hölder’s inequality with the actual functions. Its conjugate exponents are and . The functions and belong to by the hypotheses and Minkowski’s inequality. Thus

    The second inequality is Hölder. The next is Minkowski applied to the two scalar norm functions. The last uses . This identifies every function and exponent in the estimate without introducing new names for their norms.

  4. Take the limit and then subtract the integrals. Since , eventually it is at most . The last bound in Step 3 is then at most

    The coefficient is finite because . Together with Step 2 this proves convergence for every . The integrability checked in Step 1 now justifies

    All eventual statements and limits use the same filter ; neither finite total measure nor a sequence index was assumed.

Main citations

Lean source signature (exact)

theorem tendsto_integral_det_of_strongLn
    {n : ℕ} (hn : 0 < n) {α ι : Type*} [MeasurableSpace α]
    {l : Filter ι} {μ : Measure α}
    {P : ι → α → ((Fin n → ℝ) →L[ℝ] (Fin n → ℝ))}
    {Q : α → ((Fin n → ℝ) →L[ℝ] (Fin n → ℝ))}
    (hstrong : StrongLnOperatorField l μ P Q)
    (hQ : MemLp Q n μ) :
    Tendsto (fun i => ∫ x,
      LinearMap.det (P i x : (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ)) ∂μ) l
      (𝓝 (∫ x,
        LinearMap.det (Q x : (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ)) ∂μ))
In the source Mathematical meaning
{n : ℕ} (hn : 0 < n) The positive dimension of the real sup-norm coordinate space.
{α ι : Type*} [MeasurableSpace α] {l : Filter ι} {μ : Measure α} The measure space , index set , arbitrary filter on it, and measure ; no finiteness or sequence restriction is imposed.
{P : ι → α → ((Fin n → ℝ) →L[ℝ] (Fin n → ℝ))} {Q : α → ((Fin n → ℝ) →L[ℝ] (Fin n → ℝ))} The endomorphism fields on , with operator norm induced by the coordinate sup norm.
(hstrong : StrongLnOperatorField l μ P Q) The cited definition has two conditions: along , and eventually .
(hQ : MemLp Q n μ) The separate assumption : a.e. strong measurability and finite seminorm. It is not included in hstrong.
In the source Mathematical meaning
LinearMap.det (P i x : (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ)) The real signed determinant ; the cast keeps the same map. The analogous expression denotes .
Tendsto (fun i => ∫ x, LinearMap.det (P i x : (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ)) ∂μ) l The conclusion sends to along the same filter , as specified by the final neighbourhood expression.
Exact surrounding binder context (separate excerpt) 
noncomputable section

open Set MeasureTheory Filter
open scoped BigOperators ENNReal NNReal Topology

namespace MathlibAnnex.MeasureTheory

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Exact content identity

Declaration: MathlibAnnex.MeasureTheory.tendsto_integral_det_of_strongLn

Accepted content SHA-256: 0fc2e6a5c66ad16c8c54f93528df3635c588c0df6f331643a812852eb7ded16a

Accepted source guide SHA-256: e3f0a706712505e7e4abc489e7f2b514f24be3fe57ac5a1956708d00ac984e9e

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑