[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s
g_int : IntegrableOn g s
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (Measure.restrict μ s)] g
⊢ ↑↑(Measure.prod μ volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)
[PROOFSTEP]
have h : g - f =ᵐ[μ.restrict s] fun x => Real.toNNReal (g x - f x) :=
  hfg.mono fun x hx => (Real.coe_toNNReal _ <| sub_nonneg.2 hx).symm
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s
g_int : IntegrableOn g s
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (Measure.restrict μ s)] g
h : g - f =ᶠ[ae (Measure.restrict μ s)] fun x => ↑(Real.toNNReal (g x - f x))
⊢ ↑↑(Measure.prod μ volume) (regionBetween f g s) = ENNReal.ofReal (∫ (y : α) in s, (g - f) y ∂μ)
[PROOFSTEP]
rw [volume_regionBetween_eq_lintegral f_int.aemeasurable g_int.aemeasurable hs, integral_congr_ae h, lintegral_congr_ae,
  lintegral_coe_eq_integral _ ((integrable_congr h).mp (g_int.sub f_int))]
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s
g_int : IntegrableOn g s
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (Measure.restrict μ s)] g
h : g - f =ᶠ[ae (Measure.restrict μ s)] fun x => ↑(Real.toNNReal (g x - f x))
⊢ (fun y => ENNReal.ofReal ((g - f) y)) =ᶠ[ae (Measure.restrict μ s)] fun a => ↑(Real.toNNReal (g a - f a))
[PROOFSTEP]
dsimp only
[GOAL]
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
s : Set α
inst✝ : SigmaFinite μ
f_int : IntegrableOn f s
g_int : IntegrableOn g s
hs : MeasurableSet s
hfg : f ≤ᶠ[ae (Measure.restrict μ s)] g
h : g - f =ᶠ[ae (Measure.restrict μ s)] fun x => ↑(Real.toNNReal (g x - f x))
⊢ (fun y => ENNReal.ofReal ((g - f) y)) =ᶠ[ae (Measure.restrict μ s)] fun a => ↑(Real.toNNReal (g a - f a))
[PROOFSTEP]
rfl
[GOAL]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
⊢ Integrable ↑f
[PROOFSTEP]
refine'
  @integrable_of_summable_norm_restrict ℝ ℤ E _ volume _ _ _ _ _ _ _ _
    (summable_of_nonneg_of_le
      (fun n : ℤ =>
        mul_nonneg (norm_nonneg (f.restrict (⟨Icc (n : ℝ) ((n : ℝ) + 1), isCompact_Icc⟩ : Compacts ℝ)))
          ENNReal.toReal_nonneg)
      (fun n => _) hf)
    _
      -- porting note: `refine` was able to find that on its own before
[GOAL]
case refine'_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
⊢ ℤ → Compacts ℝ
[PROOFSTEP]
intro n
[GOAL]
case refine'_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
n : ℤ
⊢ Compacts ℝ
[PROOFSTEP]
exact ⟨Icc (n : ℝ) ((n : ℝ) + 1), isCompact_Icc⟩
[GOAL]
case refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
n : ℤ
⊢ ‖ContinuousMap.restrict (↑{ carrier := Icc (↑n) (↑n + 1), isCompact' := (_ : IsCompact (Icc (↑n) (↑n + 1))) }) f‖ *
      ENNReal.toReal (↑↑volume ↑{ carrier := Icc (↑n) (↑n + 1), isCompact' := (_ : IsCompact (Icc (↑n) (↑n + 1))) }) ≤
    ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
[PROOFSTEP]
simp only [Compacts.coe_mk, Real.volume_Icc, add_sub_cancel', ENNReal.toReal_ofReal zero_le_one, mul_one,
  norm_le _ (norm_nonneg _)]
[GOAL]
case refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
n : ℤ
⊢ ∀ (x : ↑(Icc (↑n) (↑n + 1))),
    ‖↑(ContinuousMap.restrict (Icc (↑n) (↑n + 1)) f) x‖ ≤
      ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
[PROOFSTEP]
intro x
[GOAL]
case refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
n : ℤ
x : ↑(Icc (↑n) (↑n + 1))
⊢ ‖↑(ContinuousMap.restrict (Icc (↑n) (↑n + 1)) f) x‖ ≤
    ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
[PROOFSTEP]
have :=
  ((f.comp <| ContinuousMap.addRight n).restrict (Icc 0 1)).norm_coe_le_norm
    ⟨x - n, ⟨sub_nonneg.mpr x.2.1, sub_le_iff_le_add'.mpr x.2.2⟩⟩
[GOAL]
case refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
n : ℤ
x : ↑(Icc (↑n) (↑n + 1))
this :
  ‖↑(ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n)))
        { val := ↑x - ↑n, property := (_ : 0 ≤ ↑x - ↑n ∧ ↑x - ↑n ≤ 1) }‖ ≤
    ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
⊢ ‖↑(ContinuousMap.restrict (Icc (↑n) (↑n + 1)) f) x‖ ≤
    ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
[PROOFSTEP]
simpa only [ContinuousMap.restrict_apply, comp_apply, coe_addRight, Subtype.coe_mk, sub_add_cancel] using this
[GOAL]
case refine'_3
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
⊢ ⋃ (i : ℤ), ↑{ carrier := Icc (↑i) (↑i + 1), isCompact' := (_ : IsCompact (Icc (↑i) (↑i + 1))) } = univ
[PROOFSTEP]
exact iUnion_Icc_int_cast ℝ
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x
[PROOFSTEP]
have A : MeasurableEmbedding fun x : ℝ => -x := (Homeomorph.neg ℝ).closedEmbedding.measurableEmbedding
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x => -x
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x
[PROOFSTEP]
have := MeasurableEmbedding.set_integral_map (μ := volume) A f (Ici (-c))
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x => -x
this : ∫ (y : ℝ) in Ici (-c), f y ∂Measure.map (fun x => -x) volume = ∫ (x : ℝ) in (fun x => -x) ⁻¹' Ici (-c), f (-x)
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x
[PROOFSTEP]
rw [Measure.map_neg_eq_self (volume : Measure ℝ)] at this 
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
A : MeasurableEmbedding fun x => -x
this : ∫ (y : ℝ) in Ici (-c), f y = ∫ (x : ℝ) in (fun x => -x) ⁻¹' Ici (-c), f (-x)
⊢ ∫ (x : ℝ) in Iic c, f (-x) = ∫ (x : ℝ) in Ioi (-c), f x
[PROOFSTEP]
simp_rw [← integral_Ici_eq_integral_Ioi, this, neg_preimage, preimage_neg_Ici, neg_neg]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
⊢ ∫ (x : ℝ) in Ioi c, f (-x) = ∫ (x : ℝ) in Iic (-c), f x
[PROOFSTEP]
rw [← neg_neg c, ← integral_comp_neg_Iic]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
⊢ ∫ (x : ℝ) in Iic (-c), f (- -x) = ∫ (x : ℝ) in Iic (- - -c), f x
[PROOFSTEP]
simp only [neg_neg]
