OAI/Analysis/AffineBernstein/SegmentEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.matrix_dual_cauchy line 16
2. lemma OAI.AffineBernstein.directional_derivative_sq_le line 26
3. lemma OAI.AffineBernstein.integral_pair_cauchy line 40

   Source documentation

   Integral Cauchy--Schwarz with a pointwise dual pairing. No square roots or strict positivity assumptions on the two nonnegative factors are required.

   lemma integral_pair_cauchy {X : Type*} [MeasurableSpace X] {μ : Measure X}
       {H E d : X → ℝ} (hH : Integrable H μ) (hE : Integrable E μ) (hd : Integrable d μ)
       (hHpos : ∀ x, 0 ≤ H x) (hEpos : ∀ x, 0 ≤ E x)
       (hpair : ∀ x, (d x)^2 ≤ H x * E x) :
       (∫ x, d x ∂μ)^2 ≤ (∫ x, H x ∂μ)*(∫ x, E x ∂μ) := by
   …

4. lemma OAI.AffineBernstein.segment_energy_bound line 61