FiniteBilinearAE.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A common null set for all mixed directions of finite quadratic forms

theorem OAI.RegularPointCoordinates.bilinear_coordinates line 14
theorem OAI.RegularPointCoordinates.bilinear_diagonal_continuous line 22

theorem OAI.RegularPointCoordinates.ae_bilinear_mixed_bound_of_diagonal line 30

Source documentation

Bounds established separately in each real direction yield one null set outside which every mixed-direction bound holds.

theorem ae_bilinear_mixed_bound_of_diagonal {X : Type*} [MeasurableSpace X] (μ : Measure X)
    (P H : X → Euclidean m →ₗ[ℝ] Euclidean m →ₗ[ℝ] ℝ) (b : X → ℝ)
    (hP : ∀ x a c, P x a c=P x c a) (hH : ∀ x a c, H x a c=H x c a)
    (hpos : ∀ a, ∀ᵐ x ∂μ, 0≤P x a a) (hb : ∀ᵐ x ∂μ, 0≤b x)
    (hdiag : ∀ a, ∀ᵐ x ∂μ, (H x a a)^2≤b x*(P x a a)^2) :
    ∀ᵐ x ∂μ, ∀ a c, (H x a c)^2≤b x*P x a a*P x c c := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean