Skip to content

Commit

Permalink
move to rclike section
Browse files Browse the repository at this point in the history
  • Loading branch information
arulandu committed Oct 10, 2024
1 parent 1e7c736 commit b772cd7
Showing 1 changed file with 25 additions and 23 deletions.
48 changes: 25 additions & 23 deletions Mathlib/MeasureTheory/Integral/IntegrableOn.lean
Original file line number Diff line number Diff line change
Expand Up @@ -338,6 +338,31 @@ theorem IntegrableOn.setLIntegral_lt_top {f : α → ℝ} {s : Set α} (hf : Int
@[deprecated (since := "2024-06-29")]
alias IntegrableOn.set_lintegral_lt_top := IntegrableOn.setLIntegral_lt_top

section RCLike

variable {𝕜 : Type*} [RCLike 𝕜]

theorem IntegrableOn.iff_ofReal {f : α → ℝ} :
IntegrableOn f s μ ↔ IntegrableOn (fun x ↦ (f x : ℂ)) s μ :=
MeasureTheory.Integrable.iff_ofReal

theorem IntegrableOn.ofReal {f : α → ℝ} (hf : IntegrableOn f s μ) :
IntegrableOn (fun x => (f x : 𝕜)) s μ := by
rw [IntegrableOn, ← memℒp_one_iff_integrable] at hf ⊢
exact hf.ofReal

theorem IntegrableOn.re_im_iff {f : α → 𝕜} :
IntegrableOn (fun x => RCLike.re (f x)) s μ ∧ IntegrableOn (fun x => RCLike.im (f x)) s μ ↔
IntegrableOn f s μ := Integrable.re_im_iff (f := f)

theorem IntegrableOn.re {f : α → 𝕜} (hf : IntegrableOn f s μ) :
IntegrableOn (fun x => RCLike.re (f x)) s μ := (IntegrableOn.re_im_iff.2 hf).left

theorem IntegrableOn.im {f : α → 𝕜} (hf : IntegrableOn f s μ) :
IntegrableOn (fun x => RCLike.im (f x)) s μ := (IntegrableOn.re_im_iff.2 hf).right

end RCLike

/-- We say that a function `f` is *integrable at filter* `l` if it is integrable on some
set `s ∈ l`. Equivalently, it is eventually integrable on `s` in `l.smallSets`. -/
def IntegrableAtFilter (f : α → E) (l : Filter α) (μ : Measure α := by volume_tac) :=
Expand Down Expand Up @@ -695,26 +720,3 @@ theorem integrableOn_Iic_iff_integrableOn_Iio :
integrableOn_Iic_iff_integrableOn_Iio' (by rw [measure_singleton]; exact ENNReal.zero_ne_top)

end PartialOrder

namespace MeasureTheory
variable {X : Type*} [MeasurableSpace X] {𝕜 : Type*} [RCLike 𝕜] {μ : Measure X} {s : Set X}
theorem IntegrableOn.iff_ofReal {f : X → ℝ} :
IntegrableOn f s μ ↔ IntegrableOn (fun x ↦ (f x : ℂ)) s μ :=
MeasureTheory.Integrable.iff_ofReal

theorem IntegrableOn.ofReal {f : X → ℝ} (hf : IntegrableOn f s μ) :
IntegrableOn (fun x => (f x : 𝕜)) s μ := by
rw [IntegrableOn, ← memℒp_one_iff_integrable] at hf ⊢
exact hf.ofReal

theorem IntegrableOn.re_im_iff {f : X → 𝕜} :
IntegrableOn (fun x => RCLike.re (f x)) s μ ∧ IntegrableOn (fun x => RCLike.im (f x)) s μ ↔
IntegrableOn f s μ := Integrable.re_im_iff (f := f)

theorem IntegrableOn.re {f : X → 𝕜} (hf : IntegrableOn f s μ) :
IntegrableOn (fun x => RCLike.re (f x)) s μ := (IntegrableOn.re_im_iff.2 hf).left

theorem IntegrableOn.im {f : X → 𝕜} (hf : IntegrableOn f s μ) :
IntegrableOn (fun x => RCLike.im (f x)) s μ := (IntegrableOn.re_im_iff.2 hf).right

end MeasureTheory

0 comments on commit b772cd7

Please sign in to comment.