FiniteDimensionalBochnerAE.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A common null set for the finite-dimensional Bochner correction

theorem OAI.RegularPointCoordinates.ae_finite_bochner_shift_nonneg line 16

Source documentation

The scalar finite-dimensional Bochner bound, initially available in each fixed direction, holds in every direction outside one null set.

theorem ae_finite_bochner_shift_nonneg {X : Type*} [MeasurableSpace X] {m : ℕ}
    (μ : Measure X) (B : X → Euclidean m →ₗ[ℝ] Euclidean m →ₗ[ℝ] ℝ)
    (D : X → Euclidean m →ₗ[ℝ] ℝ) (N : ℝ) (hN : 0<N)
    (hBE : ∀ a, ∀ᵐ x ∂μ, (D x a)^2≤N*B x a a) :
    ∀ᵐ x ∂μ, ∀ a b, 0≤B x a a-2*b*D x a+N*b^2 := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean

theorem OAI.RegularPointCoordinates.bochnerRadonDensity_diagonal line 34
Source documentation
The diagonal bilinear density equals the Radon--Nikodym density of the full positive measure.
```
theorem bochnerRadonDensity_diagonal {X : Type*} [MeasurableSpace X] {m : ℕ}
    (μ : Measure X) [SigmaFinite μ] (M : PositiveBilinearMeasure X (Euclidean m))
    (a : Euclidean m) :
    (fun x => bochnerRadonDensity μ M x a a) =ᵐ[μ]
      fun x => ((M.measure a).rnDeriv μ x).toReal := by
…
```
Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.bochnerRadonDensity

theorem OAI.RegularPointCoordinates.shiftedBochnerLowerBound_of_finite_dimension line 45

Source documentation

The scalar dimensional inequality gives the full shifted measure lower bound, with no absolute-continuity assumption on its Bochner mass.

theorem shiftedBochnerLowerBound_of_finite_dimension {X : Type*} [MeasurableSpace X] {m : ℕ}
    (μ : Measure X) [SigmaFinite μ] (M : PositiveBilinearMeasure X (Euclidean m))
    {Ω : Set X} [IsFiniteMeasure (μ.restrict Ω)]
    (ell : Euclidean m →ₗ[ℝ] ℝ) (N : ℝ) (hN : 0<N)
    (hBE : ∀ a, ∀ᵐ x ∂μ.restrict Ω,
      (ell a)^2≤N*bochnerRadonDensity μ M x a a) :
    ShiftedBochnerLowerBound M (μ.restrict Ω) ell N := by
…

Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.bochnerRadonDensity, OAI.RegularPointCoordinates.ShiftedBochnerLowerBound