/-
 - Created in 2024 by Gaëtan Serré
-/

/-
- https://github.com/gaetanserre/SBS-Proofs
-/

import Mathlib.MeasureTheory.Function.AEEqOfIntegral

import SBSProofs.Bijection

open ENNReal MeasureTheory

set_option maxHeartbeats 400000

variable {α β : Type*} [MeasureSpace α]

/-
  Definition of pushforward measure
-/

def measure_set_of_pushforward_measure [MeasureSpace β]
    (μ : Measure α) (p_μ : Measure β) (f : β → α) :=
  ∀ (B : Set β), p_μ B = μ (f '' B)

def push_forward_integration [MeasureSpace β]
    (μ : Measure α) (p_μ : Measure β) (T : α → β) (T_inv : β → α) :=
  ∀ (φ : β → ℝ), ∀ (B : Set β), ∫ x in B, φ x ∂p_μ = ∫ x in T_inv '' B, (φ ∘ T) x ∂μ

structure Pushforward_Measure (α β : Type*) [MeasureSpace α] [MeasureSpace β] where
  p_μ : Measure β
  μ : Measure α
  T : α → β
  T_inv : β → α
  measure_app : measure_set_of_pushforward_measure μ p_μ T_inv
  is_bij : is_bijective T
  is_reci : is_reciprocal T T_inv
  integration : push_forward_integration μ p_μ T T_inv

/--
  Definition of measure with density w.r.t. the Lesbegue measure.
-/
structure DensityMeasure (α : Type*) [MeasureSpace α] extends Measure α where
  d : α → ℝ≥0∞
  d_neq_top : ∀ x, d x ≠ ⊤
  d_measurable : Measurable d
  d_finite : ∫⁻ x, d x ≠ ∞
  lebesgue_density : toMeasure = volume.withDensity d

variable {μ : Measure α}

theorem fun_ae_imp_set_ae {f g : α → β} :
    f =ᵐ[μ] g ↔ ∀ (s : Set α), ∀ᵐ x ∂ μ, x ∈ s → f x = g x :=
  Iff.intro
  (λ h s ↦ 
Goals accomplished!by
Goals accomplished!
Goals accomplished! 🐙 
Goals accomplished!
α: Type u_1
β: Type u_2
inst✝: MeasureSpace α
μ: Measure α
f, g: α → β
h: f =ᶠ[ae μ] g
s: Set α
∀ᵐ (x : α) ∂μ, x ∈ s → f x = g xfilter_upwards [h] with _ ha _ using ha
Goals accomplished!
Goals accomplished! 🐙)
  (λ h ↦ 
Goals accomplished!by
Goals accomplished!
Goals accomplished! 🐙 
Goals accomplished!
α: Type u_1
β: Type u_2
inst✝: MeasureSpace α
μ: Measure α
f, g: α → β
h: ∀ (s : Set α), ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
f =ᶠ[ae μ] gfilter_upwards [h Set.univ] with _ ha using (ha (trivial))
Goals accomplished!
Goals accomplished! 🐙)
Goals accomplished!

lemma coe_ae {μ : Measure α} {f g : α → ℝ≥0∞} (h : f =ᵐ[μ] g) : (λ x ↦ (f x).toReal) =ᵐ[μ] (λ x ↦ (g x).toReal) := 
Goals accomplished!by
Goals accomplished!
Goals accomplished! 🐙

  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
(fun x => (f x).toReal) =ᶠ[ae μ] fun x => (g x).toRealhave compl_ss : {x | (f x).toReal = (g x).toReal}ᶜ ⊆ {x | f x = g x}ᶜ := 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
(fun x => (f x).toReal) =ᶠ[ae μ] fun x => (g x).toRealby
Goals accomplished!
Goals accomplished! 🐙 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
{x | (f x).toReal = (g x).toReal}ᶜ ⊆ {x | f x = g x}ᶜ{
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
{x | (f x).toReal = (g x).toReal}ᶜ ⊆ {x | f x = g x}ᶜ
    
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
{x | (f x).toReal = (g x).toReal}ᶜ ⊆ {x | f x = g x}ᶜhave eq_ss : {x | f x = g x} ⊆ {x | (f x).toReal = (g x).toReal} := 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
{x | (f x).toReal = (g x).toReal}ᶜ ⊆ {x | f x = g x}ᶜby
Goals accomplished!
Goals accomplished! 🐙 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
{x | f x = g x} ⊆ {x | (f x).toReal = (g x).toReal}{
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
{x | f x = g x} ⊆ {x | (f x).toReal = (g x).toReal}
      
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
{x | f x = g x} ⊆ {x | (f x).toReal = (g x).toReal}intro x (hx : f x = g x)
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
x: α
hx: f x = g x
x ∈ {x | (f x).toReal = (g x).toReal}
      
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
{x | f x = g x} ⊆ {x | (f x).toReal = (g x).toReal}exact congrArg ENNReal.toReal hx
Goals accomplished!
Goals accomplished! 🐙
    }
Goals accomplished!
Goals accomplished! 🐙
    
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
{x | (f x).toReal = (g x).toReal}ᶜ ⊆ {x | f x = g x}ᶜexact Set.compl_subset_compl_of_subset eq_ss
Goals accomplished!
Goals accomplished! 🐙
  }
Goals accomplished!
Goals accomplished! 🐙

  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
(fun x => (f x).toReal) =ᶠ[ae μ] fun x => (g x).toRealhave leq_μ : μ {x | (f x).toReal = (g x).toReal}ᶜ <= μ {x | f x = g x}ᶜ := measure_mono compl_ss
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
compl_ss: {x | (f x).toReal = (g x).toReal}ᶜ ⊆ {x | f x = g x}ᶜ
leq_μ: μ {x | (f x).toReal = (g x).toReal}ᶜ ≤ μ {x | f x = g x}ᶜ
(fun x => (f x).toReal) =ᶠ[ae μ] fun x => (g x).toReal

  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
(fun x => (f x).toReal) =ᶠ[ae μ] fun x => (g x).toRealhave h_ae: μ {x | f x ≠ g x} = 0 := h
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
compl_ss: {x | (f x).toReal = (g x).toReal}ᶜ ⊆ {x | f x = g x}ᶜ
leq_μ: μ {x | (f x).toReal = (g x).toReal}ᶜ ≤ μ {x | f x = g x}ᶜ
h_ae: μ {x | f x ≠ g x} = 0
(fun x => (f x).toReal) =ᶠ[ae μ] fun x => (g x).toReal
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
(fun x => (f x).toReal) =ᶠ[ae μ] fun x => (g x).toRealrw [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
compl_ss: {x | (f x).toReal = (g x).toReal}ᶜ ⊆ {x | f x = g x}ᶜ
leq_μ: μ {x | (f x).toReal = (g x).toReal}ᶜ ≤ μ {x | f x = g x}ᶜ
h_ae: μ {x | f x ≠ g x} = 0
(fun x => (f x).toReal) =ᶠ[ae μ] fun x => (g x).toRealh
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
compl_ss: {x | (f x).toReal = (g x).toReal}ᶜ ⊆ {x | f x = g x}ᶜ
leq_μ: μ {x | (f x).toReal = (g x).toReal}ᶜ ≤ 0
h_ae: μ {x | f x ≠ g x} = 0
(fun x => (f x).toReal) =ᶠ[ae μ] fun x => (g x).toReal]
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
compl_ss: {x | (f x).toReal = (g x).toReal}ᶜ ⊆ {x | f x = g x}ᶜ
leq_μ: μ {x | (f x).toReal = (g x).toReal}ᶜ ≤ 0
h_ae: μ {x | f x ≠ g x} = 0
(fun x => (f x).toReal) =ᶠ[ae μ] fun x => (g x).toReal at leq_μ
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
compl_ss: {x | (f x).toReal = (g x).toReal}ᶜ ⊆ {x | f x = g x}ᶜ
leq_μ: μ {x | (f x).toReal = (g x).toReal}ᶜ ≤ 0
h_ae: μ {x | f x ≠ g x} = 0
(fun x => (f x).toReal) =ᶠ[ae μ] fun x => (g x).toReal
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: Measure α
f, g: α → ℝ≥0∞
h: f =ᶠ[ae μ] g
(fun x => (f x).toReal) =ᶠ[ae μ] fun x => (g x).toRealexact nonpos_iff_eq_zero.mp leq_μ
Goals accomplished!
Goals accomplished! 🐙

namespace DensityMeasure

instance instCoeFun : CoeFun (DensityMeasure α) λ _ => Set α → ℝ≥0∞ := ⟨fun m => m.toMeasure⟩

theorem is_density (μ : DensityMeasure α) : ∀ ⦃s⦄, MeasurableSet s → μ s = ∫⁻ x in s, μ.d x := 
Goals accomplished!by
Goals accomplished!
Goals accomplished! 🐙
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
∀ ⦃s : Set α⦄, MeasurableSet s → μ.toMeasure s = ∫⁻ (x : α) in s, μ.d xintro s hs
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
s: Set α
hs: MeasurableSet s
μ.toMeasure s = ∫⁻ (x : α) in s, μ.d x
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
∀ ⦃s : Set α⦄, MeasurableSet s → μ.toMeasure s = ∫⁻ (x : α) in s, μ.d xrw [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
s: Set α
hs: MeasurableSet s
μ.toMeasure s = ∫⁻ (x : α) in s, μ.d x←withDensity_apply μ.d hs
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
s: Set α
hs: MeasurableSet s
μ.toMeasure s = (volume.withDensity μ.d) s]
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
s: Set α
hs: MeasurableSet s
μ.toMeasure s = (volume.withDensity μ.d) s
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
∀ ⦃s : Set α⦄, MeasurableSet s → μ.toMeasure s = ∫⁻ (x : α) in s, μ.d xexact congrFun (congrArg OuterMeasure.measureOf (congrArg Measure.toOuterMeasure μ.lebesgue_density)) s
Goals accomplished!
Goals accomplished! 🐙

lemma density_integration {μ : DensityMeasure α} {f : α → ℝ} (hi : Integrable f μ.toMeasure)
    (hm_up : Measurable (λ x ↦ ENNReal.ofReal (f x)))
    (hm_lo : Measurable (λ x ↦ ENNReal.ofReal (-f x)))
    (hi_mul : Integrable (λ x ↦ (μ.d x).toReal * f x)) :
    ∫ x, f x ∂μ.toMeasure = ∫ x, ENNReal.toReal (μ.d x) * f x := 
Goals accomplished!by
Goals accomplished!
Goals accomplished! 🐙

  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
∫ (x : α), f x ∂μ.toMeasure = ∫ (x : α), (μ.d x).toReal * f xrw [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
∫ (x : α), f x ∂μ.toMeasure = ∫ (x : α), (μ.d x).toReal * f xintegral_eq_lintegral_pos_part_sub_lintegral_neg_part hi,
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
(∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ.toMeasure).toReal - (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂μ.toMeasure).toReal =
  ∫ (x : α), (μ.d x).toReal * f x 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
∫ (x : α), f x ∂μ.toMeasure = ∫ (x : α), (μ.d x).toReal * f xμ.lebesgue_density
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
(∫⁻ (a : α), ENNReal.ofReal (f a) ∂volume.withDensity μ.d).toReal -
    (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂volume.withDensity μ.d).toReal =
  ∫ (x : α), (μ.d x).toReal * f x]
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
(∫⁻ (a : α), ENNReal.ofReal (f a) ∂volume.withDensity μ.d).toReal -
    (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂volume.withDensity μ.d).toReal =
  ∫ (x : α), (μ.d x).toReal * f x
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
∫ (x : α), f x ∂μ.toMeasure = ∫ (x : α), (μ.d x).toReal * f xrw [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
(∫⁻ (a : α), ENNReal.ofReal (f a) ∂volume.withDensity μ.d).toReal -
    (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂volume.withDensity μ.d).toReal =
  ∫ (x : α), (μ.d x).toReal * f xlintegral_withDensity_eq_lintegral_mul volume μ.d_measurable hm_up
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
(∫⁻ (a : α), (μ.d * fun x => ENNReal.ofReal (f x)) a).toReal -
    (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂volume.withDensity μ.d).toReal =
  ∫ (x : α), (μ.d x).toReal * f x]
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
(∫⁻ (a : α), (μ.d * fun x => ENNReal.ofReal (f x)) a).toReal -
    (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂volume.withDensity μ.d).toReal =
  ∫ (x : α), (μ.d x).toReal * f x
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
∫ (x : α), f x ∂μ.toMeasure = ∫ (x : α), (μ.d x).toReal * f xrw [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
(∫⁻ (a : α), (μ.d * fun x => ENNReal.ofReal (f x)) a).toReal -
    (∫⁻ (a : α), ENNReal.ofReal (-f a) ∂volume.withDensity μ.d).toReal =
  ∫ (x : α), (μ.d x).toReal * f xlintegral_withDensity_eq_lintegral_mul volume μ.d_measurable hm_lo
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
(∫⁻ (a : α), (μ.d * fun x => ENNReal.ofReal (f x)) a).toReal -
    (∫⁻ (a : α), (μ.d * fun x => ENNReal.ofReal (-f x)) a).toReal =
  ∫ (x : α), (μ.d x).toReal * f x]
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
(∫⁻ (a : α), (μ.d * fun x => ENNReal.ofReal (f x)) a).toReal -
    (∫⁻ (a : α), (μ.d * fun x => ENNReal.ofReal (-f x)) a).toReal =
  ∫ (x : α), (μ.d x).toReal * f x

  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
∫ (x : α), f x ∂μ.toMeasure = ∫ (x : α), (μ.d x).toReal * f xhave rw_fun : ∀ (f : α → ℝ), ∀ a, (μ.d * (λ a ↦ ENNReal.ofReal (f a))) a = μ.d a * ENNReal.ofReal (f a) := 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
(∫⁻ (a : α), (μ.d * fun x => ENNReal.ofReal (f x)) a).toReal -
    (∫⁻ (a : α), (μ.d * fun x => ENNReal.ofReal (-f x)) a).toReal =
  ∫ (x : α), (μ.d x).toReal * f xby
Goals accomplished!
Goals accomplished! 🐙 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a){
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
    
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)intro f a
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f✝: α → ℝ
hi: Integrable f✝ μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f✝ x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f✝ x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f✝ x) volume
f: α → ℝ
a: α
(μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
    
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)rfl
Goals accomplished!
Goals accomplished! 🐙
  }
Goals accomplished!
Goals accomplished! 🐙
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
∫ (x : α), f x ∂μ.toMeasure = ∫ (x : α), (μ.d x).toReal * f xsimp_rw [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
(∫⁻ (a : α), (μ.d * fun x => ENNReal.ofReal (f x)) a).toReal -
    (∫⁻ (a : α), (μ.d * fun x => ENNReal.ofReal (-f x)) a).toReal =
  ∫ (x : α), (μ.d x).toReal * f xrw_fun f,
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
(∫⁻ (a : α), μ.d a * ENNReal.ofReal (f a)).toReal - (∫⁻ (a : α), (μ.d * fun x => ENNReal.ofReal (-f x)) a).toReal =
  ∫ (x : α), (μ.d x).toReal * f x 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
(∫⁻ (a : α), (μ.d * fun x => ENNReal.ofReal (f x)) a).toReal -
    (∫⁻ (a : α), (μ.d * fun x => ENNReal.ofReal (-f x)) a).toReal =
  ∫ (x : α), (μ.d x).toReal * f xrw_fun (λ x ↦ -f x)
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
(∫⁻ (a : α), μ.d a * ENNReal.ofReal (f a)).toReal - (∫⁻ (a : α), μ.d a * ENNReal.ofReal (-f a)).toReal =
  ∫ (x : α), (μ.d x).toReal * f x]
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
(∫⁻ (a : α), μ.d a * ENNReal.ofReal (f a)).toReal - (∫⁻ (a : α), μ.d a * ENNReal.ofReal (-f a)).toReal =
  ∫ (x : α), (μ.d x).toReal * f x

  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
∫ (x : α), f x ∂μ.toMeasure = ∫ (x : α), (μ.d x).toReal * f xhave coe_density_nonneg : ∀ a, 0 <= (μ.d a).toReal := λ a ↦ toReal_nonneg
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
(∫⁻ (a : α), μ.d a * ENNReal.ofReal (f a)).toReal - (∫⁻ (a : α), μ.d a * ENNReal.ofReal (-f a)).toReal =
  ∫ (x : α), (μ.d x).toReal * f x

  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
∫ (x : α), f x ∂μ.toMeasure = ∫ (x : α), (μ.d x).toReal * f xhave enn_up_coe : ∀ a, ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a) := 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
(∫⁻ (a : α), μ.d a * ENNReal.ofReal (f a)).toReal - (∫⁻ (a : α), μ.d a * ENNReal.ofReal (-f a)).toReal =
  ∫ (x : α), (μ.d x).toReal * f xby
Goals accomplished!
Goals accomplished! 🐙 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a){
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
    
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)intro a
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
a: α
ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
    
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)rw (config := {occs := .pos [2]}) [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
a: α
ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)←ofReal_toReal_eq_iff.mpr (μ.d_neq_top a)
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
a: α
ENNReal.ofReal ((μ.d a).toReal * f a) = ENNReal.ofReal (μ.d a).toReal * ENNReal.ofReal (f a)]
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
a: α
ENNReal.ofReal ((μ.d a).toReal * f a) = ENNReal.ofReal (μ.d a).toReal * ENNReal.ofReal (f a)
    
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)exact ofReal_mul (coe_density_nonneg a)
Goals accomplished!
Goals accomplished! 🐙
  }
Goals accomplished!
Goals accomplished! 🐙
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
∫ (x : α), f x ∂μ.toMeasure = ∫ (x : α), (μ.d x).toReal * f xsimp_rw [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
(∫⁻ (a : α), μ.d a * ENNReal.ofReal (f a)).toReal - (∫⁻ (a : α), μ.d a * ENNReal.ofReal (-f a)).toReal =
  ∫ (x : α), (μ.d x).toReal * f x←enn_up_coe
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
(∫⁻ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a)).toReal - (∫⁻ (a : α), μ.d a * ENNReal.ofReal (-f a)).toReal =
  ∫ (x : α), (μ.d x).toReal * f x]
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
(∫⁻ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a)).toReal - (∫⁻ (a : α), μ.d a * ENNReal.ofReal (-f a)).toReal =
  ∫ (x : α), (μ.d x).toReal * f x

  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
∫ (x : α), f x ∂μ.toMeasure = ∫ (x : α), (μ.d x).toReal * f xhave enn_lo_coe :
      ∀ a, ENNReal.ofReal (-((μ.d a).toReal * (f a))) = μ.d a * ENNReal.ofReal (-f a) := 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
(∫⁻ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a)).toReal - (∫⁻ (a : α), μ.d a * ENNReal.ofReal (-f a)).toReal =
  ∫ (x : α), (μ.d x).toReal * f xby
Goals accomplished!
Goals accomplished! 🐙 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
∀ (a : α), ENNReal.ofReal (-((μ.d a).toReal * f a)) = μ.d a * ENNReal.ofReal (-f a){
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
∀ (a : α), ENNReal.ofReal (-((μ.d a).toReal * f a)) = μ.d a * ENNReal.ofReal (-f a)
    
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
∀ (a : α), ENNReal.ofReal (-((μ.d a).toReal * f a)) = μ.d a * ENNReal.ofReal (-f a)intro a
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
a: α
ENNReal.ofReal (-((μ.d a).toReal * f a)) = μ.d a * ENNReal.ofReal (-f a)
    
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
∀ (a : α), ENNReal.ofReal (-((μ.d a).toReal * f a)) = μ.d a * ENNReal.ofReal (-f a)rw [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
a: α
ENNReal.ofReal (-((μ.d a).toReal * f a)) = μ.d a * ENNReal.ofReal (-f a)show -((μ.d a).toReal * (f a)) = (μ.d a).toReal * (-f a) by 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
a: α
ENNReal.ofReal (-((μ.d a).toReal * f a)) = μ.d a * ENNReal.ofReal (-f a)ring
Goals accomplished!
Goals accomplished! 🐙]
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
a: α
ENNReal.ofReal ((μ.d a).toReal * -f a) = μ.d a * ENNReal.ofReal (-f a)
    
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
∀ (a : α), ENNReal.ofReal (-((μ.d a).toReal * f a)) = μ.d a * ENNReal.ofReal (-f a)rw (config := {occs := .pos [2]}) [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
a: α
ENNReal.ofReal ((μ.d a).toReal * -f a) = μ.d a * ENNReal.ofReal (-f a)←ofReal_toReal_eq_iff.mpr (μ.d_neq_top a)
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
a: α
ENNReal.ofReal ((μ.d a).toReal * -f a) = ENNReal.ofReal (μ.d a).toReal * ENNReal.ofReal (-f a)]
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
a: α
ENNReal.ofReal ((μ.d a).toReal * -f a) = ENNReal.ofReal (μ.d a).toReal * ENNReal.ofReal (-f a)
    
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
∀ (a : α), ENNReal.ofReal (-((μ.d a).toReal * f a)) = μ.d a * ENNReal.ofReal (-f a)exact ofReal_mul (coe_density_nonneg a)
Goals accomplished!
Goals accomplished! 🐙
  }
Goals accomplished!
Goals accomplished! 🐙
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
∫ (x : α), f x ∂μ.toMeasure = ∫ (x : α), (μ.d x).toReal * f xsimp_rw [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
enn_lo_coe: ∀ (a : α), ENNReal.ofReal (-((μ.d a).toReal * f a)) = μ.d a * ENNReal.ofReal (-f a)
(∫⁻ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a)).toReal - (∫⁻ (a : α), μ.d a * ENNReal.ofReal (-f a)).toReal =
  ∫ (x : α), (μ.d x).toReal * f x←enn_lo_coe
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
enn_lo_coe: ∀ (a : α), ENNReal.ofReal (-((μ.d a).toReal * f a)) = μ.d a * ENNReal.ofReal (-f a)
(∫⁻ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a)).toReal -
    (∫⁻ (a : α), ENNReal.ofReal (-((μ.d a).toReal * f a))).toReal =
  ∫ (x : α), (μ.d x).toReal * f x]
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
enn_lo_coe: ∀ (a : α), ENNReal.ofReal (-((μ.d a).toReal * f a)) = μ.d a * ENNReal.ofReal (-f a)
(∫⁻ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a)).toReal -
    (∫⁻ (a : α), ENNReal.ofReal (-((μ.d a).toReal * f a))).toReal =
  ∫ (x : α), (μ.d x).toReal * f x

  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
∫ (x : α), f x ∂μ.toMeasure = ∫ (x : α), (μ.d x).toReal * f xrw[
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
enn_lo_coe: ∀ (a : α), ENNReal.ofReal (-((μ.d a).toReal * f a)) = μ.d a * ENNReal.ofReal (-f a)
(∫⁻ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a)).toReal -
    (∫⁻ (a : α), ENNReal.ofReal (-((μ.d a).toReal * f a))).toReal =
  ∫ (x : α), (μ.d x).toReal * f x←integral_eq_lintegral_pos_part_sub_lintegral_neg_part hi_mul
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ
hi: Integrable f μ.toMeasure
hm_up: Measurable fun x => ENNReal.ofReal (f x)
hm_lo: Measurable fun x => ENNReal.ofReal (-f x)
hi_mul: Integrable (fun x => (μ.d x).toReal * f x) volume
rw_fun: ∀ (f : α → ℝ) (a : α), (μ.d * fun a => ENNReal.ofReal (f a)) a = μ.d a * ENNReal.ofReal (f a)
coe_density_nonneg: ∀ (a : α), 0 ≤ (μ.d a).toReal
enn_up_coe: ∀ (a : α), ENNReal.ofReal ((μ.d a).toReal * f a) = μ.d a * ENNReal.ofReal (f a)
enn_lo_coe: ∀ (a : α), ENNReal.ofReal (-((μ.d a).toReal * f a)) = μ.d a * ENNReal.ofReal (-f a)
∫ (a : α), (μ.d a).toReal * f a = ∫ (x : α), (μ.d x).toReal * f x]
Goals accomplished!
Goals accomplished! 🐙

theorem density_lintegration {μ : DensityMeasure α} (f : α → ℝ≥0∞) (hm : Measurable f) :
    ∫⁻ x, f x ∂μ.toMeasure = ∫⁻ x, μ.d x * f x :=
Goals accomplished!by
Goals accomplished!
Goals accomplished! 🐙
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ≥0∞
hm: Measurable f
∫⁻ (x : α), f x ∂μ.toMeasure = ∫⁻ (x : α), μ.d x * f xrw [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ≥0∞
hm: Measurable f
∫⁻ (x : α), f x ∂μ.toMeasure = ∫⁻ (x : α), μ.d x * f xμ.lebesgue_density
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ≥0∞
hm: Measurable f
∫⁻ (x : α), f x ∂volume.withDensity μ.d = ∫⁻ (x : α), μ.d x * f x]
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ≥0∞
hm: Measurable f
∫⁻ (x : α), f x ∂volume.withDensity μ.d = ∫⁻ (x : α), μ.d x * f x
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ≥0∞
hm: Measurable f
∫⁻ (x : α), f x ∂μ.toMeasure = ∫⁻ (x : α), μ.d x * f xrw [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ≥0∞
hm: Measurable f
∫⁻ (x : α), f x ∂volume.withDensity μ.d = ∫⁻ (x : α), μ.d x * f xlintegral_withDensity_eq_lintegral_mul volume μ.d_measurable hm
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ≥0∞
hm: Measurable f
∫⁻ (a : α), (μ.d * f) a = ∫⁻ (x : α), μ.d x * f x]
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ≥0∞
hm: Measurable f
∫⁻ (a : α), (μ.d * f) a = ∫⁻ (x : α), μ.d x * f x
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f: α → ℝ≥0∞
hm: Measurable f
∫⁻ (x : α), f x ∂μ.toMeasure = ∫⁻ (x : α), μ.d x * f xsimp only [Pi.mul_apply]
Goals accomplished!
Goals accomplished! 🐙

@[ext]
theorem ext {μ₁ μ₂ : DensityMeasure α} (h : ∀ x, μ₁.d x = μ₂.d x) : μ₁ = μ₂ := 
Goals accomplished!by
Goals accomplished!
Goals accomplished! 🐙
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
μ₁ = μ₂have f_ext := funext h
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
f_ext: μ₁.d = μ₂.d
μ₁ = μ₂
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
μ₁ = μ₂have eq_measure : μ₁.toMeasure = μ₂.toMeasure := 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
f_ext: μ₁.d = μ₂.d
μ₁ = μ₂by
Goals accomplished!
Goals accomplished! 🐙 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
f_ext: μ₁.d = μ₂.d
μ₁.toMeasure = μ₂.toMeasure{
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
f_ext: μ₁.d = μ₂.d
μ₁.toMeasure = μ₂.toMeasure
    
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
f_ext: μ₁.d = μ₂.d
μ₁.toMeasure = μ₂.toMeasurerw [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
f_ext: μ₁.d = μ₂.d
μ₁.toMeasure = μ₂.toMeasureμ₁.lebesgue_density,
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
f_ext: μ₁.d = μ₂.d
volume.withDensity μ₁.d = μ₂.toMeasure 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
f_ext: μ₁.d = μ₂.d
μ₁.toMeasure = μ₂.toMeasureμ₂.lebesgue_density,
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
f_ext: μ₁.d = μ₂.d
volume.withDensity μ₁.d = volume.withDensity μ₂.d 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
f_ext: μ₁.d = μ₂.d
μ₁.toMeasure = μ₂.toMeasuref_ext
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
f_ext: μ₁.d = μ₂.d
volume.withDensity μ₂.d = volume.withDensity μ₂.d]
Goals accomplished!
Goals accomplished! 🐙
  }
Goals accomplished!
Goals accomplished! 🐙

  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
μ₁ = μ₂have destruct : μ₁ = {
      toMeasure := μ₁.toMeasure,
        d := μ₁.d,
        d_neq_top := μ₁.d_neq_top,
        d_measurable := μ₁.d_measurable,
        d_finite := μ₁.d_finite
      lebesgue_density := μ₁.lebesgue_density
      } := rfl
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
f_ext: μ₁.d = μ₂.d
eq_measure: μ₁.toMeasure = μ₂.toMeasure
destruct: μ₁ =
  let __Measure := μ₁.toMeasure;
  { toMeasure := __Measure, d := μ₁.d, d_neq_top := ⋯, d_measurable := ⋯, d_finite := ⋯, lebesgue_density := ⋯ }
μ₁ = μ₂

  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
μ₁ = μ₂rewrite (config := {occs := .pos [1]}) [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
f_ext: μ₁.d = μ₂.d
eq_measure: μ₁.toMeasure = μ₂.toMeasure
destruct: μ₁ =
  let __Measure := μ₁.toMeasure;
  { toMeasure := __Measure, d := μ₁.d, d_neq_top := ⋯, d_measurable := ⋯, d_finite := ⋯, lebesgue_density := ⋯ }
μ₁ = μ₂destruct
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
f_ext: μ₁.d = μ₂.d
eq_measure: μ₁.toMeasure = μ₂.toMeasure
destruct: μ₁ =
  let __Measure := μ₁.toMeasure;
  { toMeasure := __Measure, d := μ₁.d, d_neq_top := ⋯, d_measurable := ⋯, d_finite := ⋯, lebesgue_density := ⋯ }
(let __Measure := μ₁.toMeasure;
  { toMeasure := __Measure, d := μ₁.d, d_neq_top := ⋯, d_measurable := ⋯, d_finite := ⋯, lebesgue_density := ⋯ }) =
  μ₂]
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
f_ext: μ₁.d = μ₂.d
eq_measure: μ₁.toMeasure = μ₂.toMeasure
destruct: μ₁ =
  let __Measure := μ₁.toMeasure;
  { toMeasure := __Measure, d := μ₁.d, d_neq_top := ⋯, d_measurable := ⋯, d_finite := ⋯, lebesgue_density := ⋯ }
(let __Measure := μ₁.toMeasure;
  { toMeasure := __Measure, d := μ₁.d, d_neq_top := ⋯, d_measurable := ⋯, d_finite := ⋯, lebesgue_density := ⋯ }) =
  μ₂
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
μ₁ = μ₂simp_rw [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
f_ext: μ₁.d = μ₂.d
eq_measure: μ₁.toMeasure = μ₂.toMeasure
destruct: μ₁ =
  let __Measure := μ₁.toMeasure;
  { toMeasure := __Measure, d := μ₁.d, d_neq_top := ⋯, d_measurable := ⋯, d_finite := ⋯, lebesgue_density := ⋯ }
{ toMeasure := μ₁.toMeasure, d := μ₁.d, d_neq_top := ⋯, d_measurable := ⋯, d_finite := ⋯, lebesgue_density := ⋯ } = μ₂eq_measure,
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
f_ext: μ₁.d = μ₂.d
eq_measure: μ₁.toMeasure = μ₂.toMeasure
destruct: μ₁ =
  let __Measure := μ₁.toMeasure;
  { toMeasure := __Measure, d := μ₁.d, d_neq_top := ⋯, d_measurable := ⋯, d_finite := ⋯, lebesgue_density := ⋯ }
{ toMeasure := μ₂.toMeasure, d := μ₁.d, d_neq_top := ⋯, d_measurable := ⋯, d_finite := ⋯, lebesgue_density := ⋯ } = μ₂ 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
h: ∀ (x : α), μ₁.d x = μ₂.d x
f_ext: μ₁.d = μ₂.d
eq_measure: μ₁.toMeasure = μ₂.toMeasure
destruct: μ₁ =
  let __Measure := μ₁.toMeasure;
  { toMeasure := __Measure, d := μ₁.d, d_neq_top := ⋯, d_measurable := ⋯, d_finite := ⋯, lebesgue_density := ⋯ }
(let __Measure := μ₁.toMeasure;
  { toMeasure := __Measure, d := μ₁.d, d_neq_top := ⋯, d_measurable := ⋯, d_finite := ⋯, lebesgue_density := ⋯ }) =
  μ₂f_ext
Goals accomplished!
Goals accomplished! 🐙]
Goals accomplished!
Goals accomplished! 🐙


lemma coe_ext_measure (μ₁ μ₂ : Measure α) (h : ∀ s, MeasurableSet s → μ₁ s = μ₂ s) : μ₁ = μ₂ :=
  Measure.ext_iff.mpr h
Goals accomplished!

theorem densities_ae_eq_iff_eq_measure {μ₁ μ₂ : DensityMeasure α} :
    μ₁.d =ᵐ[volume] μ₂.d ↔ μ₁.toMeasure = μ₂.toMeasure := 
Goals accomplished!by
Goals accomplished!
Goals accomplished! 🐙
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
μ₁.d =ᶠ[ae volume] μ₂.d ↔ μ₁.toMeasure = μ₂.toMeasurerw [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
μ₁.d =ᶠ[ae volume] μ₂.d ↔ μ₁.toMeasure = μ₂.toMeasureμ₁.lebesgue_density,
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
μ₁.d =ᶠ[ae volume] μ₂.d ↔ volume.withDensity μ₁.d = μ₂.toMeasure 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
μ₁.d =ᶠ[ae volume] μ₂.d ↔ μ₁.toMeasure = μ₂.toMeasureμ₂.lebesgue_density
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
μ₁.d =ᶠ[ae volume] μ₂.d ↔ volume.withDensity μ₁.d = volume.withDensity μ₂.d]
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
μ₁.d =ᶠ[ae volume] μ₂.d ↔ volume.withDensity μ₁.d = volume.withDensity μ₂.d
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ₁, μ₂: DensityMeasure α
μ₁.d =ᶠ[ae volume] μ₂.d ↔ μ₁.toMeasure = μ₂.toMeasureexact (withDensity_eq_iff
    (Measurable.aemeasurable μ₁.d_measurable)
    (Measurable.aemeasurable μ₂.d_measurable)
    μ₁.d_finite).symm
Goals accomplished!
Goals accomplished! 🐙

theorem ae_density_measure_iff_ae_volume {μ : DensityMeasure α} {f g : α → ℝ≥0∞}
    (h_ae_nonneg : ∀ᵐ x, μ.d x ≠ 0) : (f =ᵐ[μ.toMeasure] g) ↔ (f =ᵐ[volume] g) := 
Goals accomplished!by
Goals accomplished!
Goals accomplished! 🐙
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
f =ᶠ[ae μ.toMeasure] g ↔ f =ᶠ[ae volume] grw [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
f =ᶠ[ae μ.toMeasure] g ↔ f =ᶠ[ae volume] gμ.lebesgue_density
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
f =ᶠ[ae (volume.withDensity μ.d)] g ↔ f =ᶠ[ae volume] g]
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
f =ᶠ[ae (volume.withDensity μ.d)] g ↔ f =ᶠ[ae volume] g
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
f =ᶠ[ae μ.toMeasure] g ↔ f =ᶠ[ae volume] gconstructor
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
mp
f =ᶠ[ae (volume.withDensity μ.d)] g → f =ᶠ[ae volume] g
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
mpr
f =ᶠ[ae volume] g → f =ᶠ[ae (volume.withDensity μ.d)] g
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
f =ᶠ[ae μ.toMeasure] g ↔ f =ᶠ[ae volume] g·
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
mp
f =ᶠ[ae (volume.withDensity μ.d)] g → f =ᶠ[ae volume] g 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
mp
f =ᶠ[ae (volume.withDensity μ.d)] g → f =ᶠ[ae volume] g
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
mpr
f =ᶠ[ae volume] g → f =ᶠ[ae (volume.withDensity μ.d)] gintro (h : ∀ᵐ x ∂(volume.withDensity μ.d), f x = g x)
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
h: ∀ᵐ (x : α) ∂volume.withDensity μ.d, f x = g x
mp
f =ᶠ[ae volume] g
    
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
mp
f =ᶠ[ae (volume.withDensity μ.d)] g → f =ᶠ[ae volume] grw [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
h: ∀ᵐ (x : α) ∂volume.withDensity μ.d, f x = g x
mp
f =ᶠ[ae volume] gae_withDensity_iff μ.d_measurable
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
h: ∀ᵐ (x : α), μ.d x ≠ 0 → f x = g x
mp
f =ᶠ[ae volume] g]
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
h: ∀ᵐ (x : α), μ.d x ≠ 0 → f x = g x
mp
f =ᶠ[ae volume] g at h
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
h: ∀ᵐ (x : α), μ.d x ≠ 0 → f x = g x
mp
f =ᶠ[ae volume] g
    
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
mp
f =ᶠ[ae (volume.withDensity μ.d)] g → f =ᶠ[ae volume] gfilter_upwards [h_ae_nonneg, h] with _ hda himp using (himp hda)
Goals accomplished!
Goals accomplished! 🐙
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
f =ᶠ[ae μ.toMeasure] g ↔ f =ᶠ[ae volume] gintro h
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
h: f =ᶠ[ae volume] g
mpr
f =ᶠ[ae (volume.withDensity μ.d)] g
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
f =ᶠ[ae μ.toMeasure] g ↔ f =ᶠ[ae volume] gsuffices ∀ᵐ x ∂(volume.withDensity μ.d), f x = g x 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
h: f =ᶠ[ae volume] g
mpr
f =ᶠ[ae (volume.withDensity μ.d)] gby
Goals accomplished!
Goals accomplished! 🐙 
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
h: f =ᶠ[ae volume] g
this: ∀ᵐ (x : α) ∂volume.withDensity μ.d, f x = g x
f =ᶠ[ae (volume.withDensity μ.d)] gexact this
Goals accomplished!
Goals accomplished! 🐙
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
f =ᶠ[ae μ.toMeasure] g ↔ f =ᶠ[ae volume] grw [
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
h: f =ᶠ[ae volume] g
mpr
∀ᵐ (x : α) ∂volume.withDensity μ.d, f x = g xae_withDensity_iff μ.d_measurable
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
h: f =ᶠ[ae volume] g
mpr
∀ᵐ (x : α), μ.d x ≠ 0 → f x = g x]
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
h: f =ᶠ[ae volume] g
mpr
∀ᵐ (x : α), μ.d x ≠ 0 → f x = g x
  
Goals accomplished!
α: Type u_1
inst✝: MeasureSpace α
μ: DensityMeasure α
f, g: α → ℝ≥0∞
h_ae_nonneg: ∀ᵐ (x : α), μ.d x ≠ 0
f =ᶠ[ae μ.toMeasure] g ↔ f =ᶠ[ae volume] gfilter_upwards [h] with _ ha _ using ha
Goals accomplished!
Goals accomplished! 🐙

end DensityMeasure