Source indexedlemma · leanprover/lean4:v4.32.0

Complex.CartanBound.intervalIntegrable_sqrt_two_div_abs_one_sub_dyadic_middle

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.CartanBound · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/CartanBound.lean:419 to 429

Mathematical statement

Exact Lean statement

lemma intervalIntegrable_sqrt_two_div_abs_one_sub_dyadic_middle {A : ℝ}
    (hA_lower : (1 / 4 : ℝ) ≤ A) (hA_upper : A ≤ (2 : ℝ)) :
    IntervalIntegrable (fun t : ℝ => Real.sqrt (2 / |1 - t|)) volume A (2 * A)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma intervalIntegrable_sqrt_two_div_abs_one_sub_dyadic_middle {A : ℝ}    (hA_lower : (1 / 4 : ℝ) ≤ A) (hA_upper : A ≤ (2 : ℝ)) :    IntervalIntegrable (fun t : ℝ => Real.sqrt (2 / |1 - t|)) volume A (2 * A) := by  have hsqrt_big :      IntervalIntegrable (fun t : ℝ => Real.sqrt (2 / |1 - t|))        (volume : MeasureTheory.Measure ℝ) (1 / 4 : ℝ) (4 : ℝ) :=    intervalIntegrable_sqrt_two_div_abs_one_sub_Icc  refine hsqrt_big.mono_set ?_  refine Set.uIcc_subset_uIcc ?_ ?_  · exact (Set.mem_uIcc).2 (Or.inl ⟨hA_lower, by nlinarith [hA_upper]⟩)  · exact (Set.mem_uIcc).2 (Or.inl ⟨by nlinarith [hA_lower], by nlinarith [hA_upper]⟩)