Bounded Trace Quadratic Derivative Data

This packages boundedness, local integrability, and weak derivative data for a trace quadratic.

Let $d,n\in\mathbb N$, let $B\in M_n(\mathbb R)$, let $A:\mathbb R^d\to M_n(\mathbb R)$, let $DA:\mathbb R^d\to M_n(\mathbb R)$ be indexed by coordinate directions, and let $M\in[0,\infty)$ be represented by an NNReal. Assume:

1. Every entry of $A$ is measurable.
2. For all $x,i,j$, $\|A_{ij}(x)\|\le M$.
3. Each entry of $A$ has the stated weak derivative $DA_k$ in the coordinate direction given by EuclideanSpace.basisFun.
4. Every entry of each $DA_k$ belongs to $L^2$ on every compact restriction of volume measure.

Then there exists $C\ge0$ such that

$$\|\operatorname{tr}(BA(x)BA(x))\|\le C$$

for every $x$, the trace quadratic is locally integrable, and for every coordinate $k$ its weak derivative is

$$2\,\operatorname{tr}(BA(x)B\,DA_k(x)),$$

with this derivative in $L^2$ on every compact set. The declaration is bounded_trace_quadratic_weak_derivative_data_readable; all finite ambient and matrix dimensions, including zero dimensions, are permitted.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem bounded_trace_quadratic_weak_derivative_data {d n : ℕ}
    (B : Matrix (Fin n) (Fin n) ℝ)
    (A : EuclideanSpace ℝ (Fin d) → Matrix (Fin n) (Fin n) ℝ)
    (DA : Fin d → EuclideanSpace ℝ (Fin d) → Matrix (Fin n) (Fin n) ℝ)
    {M : NNReal}
    (hmeas : ∀ i j, Measurable (fun x => A x i j))
    (hbound : ∀ x i j, ‖A x i j‖ ≤ (M : ℝ))
    (hweak : ∀ k i j, HasWeakDerivAlong (fun x => A x i j) (fun x => DA k x i j)
      (EuclideanSpace.basisFun (Fin d) ℝ k))
    (hDA2 : ∀ k i j, ∀ S : Set (EuclideanSpace ℝ (Fin d)), IsCompact S →
      MemLp (fun x => DA k x i j) 2
        ((volume : Measure (EuclideanSpace ℝ (Fin d))).restrict S)) :
    ∃ C : ℝ, 0 ≤ C ∧ (∀ x, ‖(B * A x * B * A x).trace‖ ≤ C) ∧
      LocallyIntegrable (fun x => (B * A x * B * A x).trace)
        (volume : Measure (EuclideanSpace ℝ (Fin d))) ∧
      ∀ k : Fin d,
        HasWeakDerivAlong (fun x => (B * A x * B * A x).trace)
          (fun x => 2 * (B * A x * B * DA k x).trace)
          (EuclideanSpace.basisFun (Fin d) ℝ k) ∧
        ∀ S : Set (EuclideanSpace ℝ (Fin d)), IsCompact S →
          MemLp (fun x => 2 * (B * A x * B * DA k x).trace) 2
            ((volume : Measure (EuclideanSpace ℝ (Fin d))).restrict S)

Module navigation

Module: Analysis/Matrix/WeakDerivative.

Definition modules: Analysis/WeakDerivative/Basic.

Supporting theorems: hasWeakDerivAlong_trace_quadratic_of_locally_memLp_two, trace_mul_mul_mul_eq_sum.

Previous: ae_weak_matrix_inverse_derivative · Next: bounded_weak_matrix_product_entry.

Source excerpt, lines 212–233 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_WeakDerivative

open MeasureTheory Set Filter Matrix

theorem FunctionalInequalities.Analysis.bounded_trace_quadratic_weak_derivative_data_readable {d n : ℕ}
    (B : Matrix (Fin n) (Fin n) ℝ)
    (A : EuclideanSpace ℝ (Fin d) → Matrix (Fin n) (Fin n) ℝ)
    (DA : Fin d → EuclideanSpace ℝ (Fin d) → Matrix (Fin n) (Fin n) ℝ)
    {M : NNReal}
    (hmeas : ∀ i j, Measurable (fun x => A x i j))
    (hbound : ∀ x i j, ‖A x i j‖ ≤ (M : ℝ))
    (hweak : ∀ k i j, HasWeakDerivAlong (fun x => A x i j) (fun x => DA k x i j)
      (EuclideanSpace.basisFun (Fin d) ℝ k))
    (hDA2 : ∀ k i j, ∀ S : Set (EuclideanSpace ℝ (Fin d)), IsCompact S →
      MemLp (fun x => DA k x i j) 2
        ((volume : Measure (EuclideanSpace ℝ (Fin d))).restrict S)) :
    ∃ C : ℝ, 0 ≤ C ∧ (∀ x, ‖(B * A x * B * A x).trace‖ ≤ C) ∧
      LocallyIntegrable (fun x => (B * A x * B * A x).trace)
        (volume : Measure (EuclideanSpace ℝ (Fin d))) ∧
      ∀ k : Fin d,
        HasWeakDerivAlong (fun x => (B * A x * B * A x).trace)
          (fun x => 2 * (B * A x * B * DA k x).trace)
          (EuclideanSpace.basisFun (Fin d) ℝ k) ∧
        ∀ S : Set (EuclideanSpace ℝ (Fin d)), IsCompact S →
          MemLp (fun x => 2 * (B * A x * B * DA k x).trace) 2
            ((volume : Measure (EuclideanSpace ℝ (Fin d))).restrict S) := by sorry