IntegratedPolarization.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Integrating the finite polarization used by the cutoff error

theorem OAI.RegularPointCoordinates.integrated_polarization_energy line 19

Source documentation

Integration of a symmetric operator family preserves the quadratic identity supplied by its finite polarizing tests.

theorem integrated_polarization_energy (B : X → Euclidean n →L[ℝ] Euclidean n)
    (hB : ∀ x, (B x).IsSymmetric)
    (hint : ∀ v, Integrable (fun x => ⟪v, B x v⟫_ℝ) μ) (v : Euclidean n) :
    ⟪v, polarizedDerivative (fun w => ∫ x, ⟪w, B x w⟫_ℝ ∂μ) v⟫_ℝ =
      ∫ x, ⟪v, B x v⟫_ℝ ∂μ := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.polarizedDerivative

theorem OAI.RegularPointCoordinates.exists_polarized_integral_bound line 46

Source documentation

One finite L1 budget controls every polarized integral operator.

theorem exists_polarized_integral_bound (g : Euclidean n → X → ℝ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (k : X → ℝ) (a : ℝ), 0 ≤ a →
      (∀ v, |∫ x, k x * g v x ∂μ| ≤ a * ∫ x, |g v x| ∂μ) →
      ‖polarizedDerivative (fun v => ∫ x, k x * g v x ∂μ)‖ ≤ C * a := by
…

Mentions: OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.polarizedDerivative