α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
⊢ setToFun μ T hT f = setToFun μ' T hT' f
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
⊢ setToFun μ T hT f = setToFun μ' T hT' f
have h_int : ∀ g : α → E, Integrable g μ → Integrable g μ' := fun g hg =>
  Integrable.of_measure_le_smul c' hc' hμ'_le hg
case h_ind
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
⊢ ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → ↑↑μ s < ⊤ → (fun f => setToFun μ T hT f = setToFun μ' T hT' f) (indicator s fun x => c)

case h_add
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
⊢ ∀ ⦃f g : α → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      Integrable f →
        Integrable g →
          (fun f => setToFun μ T hT f = setToFun μ' T hT' f) f →
            (fun f => setToFun μ T hT f = setToFun μ' T hT' f) g →
              (fun f => setToFun μ T hT f = setToFun μ' T hT' f) (f + g)

case h_closed
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
⊢ IsClosed {f | (fun f => setToFun μ T hT f = setToFun μ' T hT' f) ↑↑f}

case h_ae
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
⊢ ∀ ⦃f g : α → E⦄,
    f =ᵐ[μ] g →
      Integrable f →
        (fun f => setToFun μ T hT f = setToFun μ' T hT' f) f → (fun f => setToFun μ T hT f = setToFun μ' T hT' f) g
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
⊢ setToFun μ T hT f = setToFun μ' T hT' f
apply hfμ.induction (P := fun f => setToFun μ T hT f = setToFun μ' T hT' f)
case h_ind
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
c : E
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ setToFun μ T hT (indicator s fun x => c) = setToFun μ' T hT' (indicator s fun x => c)
case h_ind
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
⊢ ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s → ↑↑μ s < ⊤ → (fun f => setToFun μ T hT f = setToFun μ' T hT' f) (indicator s fun x => c)
intro c s hs hμs
case h_ind
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
c : E
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
hμ's : ↑↑μ' s ≠ ⊤
⊢ setToFun μ T hT (indicator s fun x => c) = setToFun μ' T hT' (indicator s fun x => c)
case h_ind
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
c : E
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ setToFun μ T hT (indicator s fun x => c) = setToFun μ' T hT' (indicator s fun x => c)
have hμ's : μ' s ≠ ∞ := by
  refine' ((hμ'_le s hs).trans_lt _).ne
  rw [Measure.smul_apply, smul_eq_mul]
  exact ENNReal.mul_lt_top hc' hμs.ne
no goals
case h_ind
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
c : E
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
hμ's : ↑↑μ' s ≠ ⊤
⊢ setToFun μ T hT (indicator s fun x => c) = setToFun μ' T hT' (indicator s fun x => c)
rw [setToFun_indicator_const hT hs hμs.ne, setToFun_indicator_const hT' hs hμ's]
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
c : E
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ↑↑(c' • μ) s < ⊤
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
c : E
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ↑↑μ' s ≠ ⊤
refine' ((hμ'_le s hs).trans_lt _).ne
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
c : E
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ c' * ↑↑μ s < ⊤
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
c : E
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ ↑↑(c' • μ) s < ⊤
rw [Measure.smul_apply, smul_eq_mul]
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
c : E
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s < ⊤
⊢ c' * ↑↑μ s < ⊤
exact ENNReal.mul_lt_top hc' hμs.ne
case h_add
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
f₂ g₂ : α → E
a✝ : Disjoint (Function.support f₂) (Function.support g₂)
hf₂ : Integrable f₂
hg₂ : Integrable g₂
h_eq_f : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
h_eq_g : setToFun μ T hT g₂ = setToFun μ' T hT' g₂
⊢ setToFun μ T hT (f₂ + g₂) = setToFun μ' T hT' (f₂ + g₂)
case h_add
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
⊢ ∀ ⦃f g : α → E⦄,
    Disjoint (Function.support f) (Function.support g) →
      Integrable f →
        Integrable g →
          (fun f => setToFun μ T hT f = setToFun μ' T hT' f) f →
            (fun f => setToFun μ T hT f = setToFun μ' T hT' f) g →
              (fun f => setToFun μ T hT f = setToFun μ' T hT' f) (f + g)
intro f₂ g₂ _ hf₂ hg₂ h_eq_f h_eq_g
no goals
case h_add
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
f₂ g₂ : α → E
a✝ : Disjoint (Function.support f₂) (Function.support g₂)
hf₂ : Integrable f₂
hg₂ : Integrable g₂
h_eq_f : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
h_eq_g : setToFun μ T hT g₂ = setToFun μ' T hT' g₂
⊢ setToFun μ T hT (f₂ + g₂) = setToFun μ' T hT' (f₂ + g₂)
rw [setToFun_add hT hf₂ hg₂, setToFun_add hT' (h_int f₂ hf₂) (h_int g₂ hg₂), h_eq_f, h_eq_g]
case h_closed
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
⊢ Continuous fun f => setToFun μ' T hT' ↑↑f
case h_closed
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
⊢ IsClosed {f | (fun f => setToFun μ T hT f = setToFun μ' T hT' f) ↑↑f}
refine' isClosed_eq (continuous_setToFun hT) _
case h_closed
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
this : (fun f => setToFun μ' T hT' ↑↑f) = fun f => setToFun μ' T hT' ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))
⊢ Continuous fun f => setToFun μ' T hT' ↑↑f
case h_closed
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
⊢ Continuous fun f => setToFun μ' T hT' ↑↑f
have :
  (fun f : α →₁[μ] E => setToFun μ' T hT' f) = fun f : α →₁[μ] E =>
    setToFun μ' T hT' ((h_int f (L1.integrable_coeFn f)).toL1 f) := by
  ext1 f; exact setToFun_congr_ae hT' (Integrable.coeFn_toL1 _).symm
case h_closed
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
this : (fun f => setToFun μ' T hT' ↑↑f) = fun f => setToFun μ' T hT' ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))
⊢ Continuous fun f => setToFun μ' T hT' ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))
case h_closed
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
this : (fun f => setToFun μ' T hT' ↑↑f) = fun f => setToFun μ' T hT' ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))
⊢ Continuous fun f => setToFun μ' T hT' ↑↑f
rw [this]
no goals
case h_closed
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
this : (fun f => setToFun μ' T hT' ↑↑f) = fun f => setToFun μ' T hT' ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))
⊢ Continuous fun f => setToFun μ' T hT' ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))
exact (continuous_setToFun hT').comp (continuous_L1_toL1 c' hc' hμ'_le)
case h
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝¹ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f✝ : α → E
hfμ : Integrable f✝
h_int : ∀ (g : α → E), Integrable g → Integrable g
f : { x // x ∈ Lp E 1 }
⊢ setToFun μ' T hT' ↑↑f = setToFun μ' T hT' ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
⊢ (fun f => setToFun μ' T hT' ↑↑f) = fun f => setToFun μ' T hT' ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))
ext1 f
no goals
case h
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝¹ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f✝ : α → E
hfμ : Integrable f✝
h_int : ∀ (g : α → E), Integrable g → Integrable g
f : { x // x ∈ Lp E 1 }
⊢ setToFun μ' T hT' ↑↑f = setToFun μ' T hT' ↑↑(Integrable.toL1 ↑↑f (_ : Integrable ↑↑f))
exact setToFun_congr_ae hT' (Integrable.coeFn_toL1 _).symm
case h_ae
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
f₂ g₂ : α → E
hfg : f₂ =ᵐ[μ] g₂
a✝ : Integrable f₂
hf_eq : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
⊢ setToFun μ T hT g₂ = setToFun μ' T hT' g₂
case h_ae
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
⊢ ∀ ⦃f g : α → E⦄,
    f =ᵐ[μ] g →
      Integrable f →
        (fun f => setToFun μ T hT f = setToFun μ' T hT' f) f → (fun f => setToFun μ T hT f = setToFun μ' T hT' f) g
intro f₂ g₂ hfg _ hf_eq
case h_ae
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
f₂ g₂ : α → E
hfg : f₂ =ᵐ[μ] g₂
a✝ : Integrable f₂
hf_eq : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
hfg' : f₂ =ᵐ[μ'] g₂
⊢ setToFun μ T hT g₂ = setToFun μ' T hT' g₂
case h_ae
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
f₂ g₂ : α → E
hfg : f₂ =ᵐ[μ] g₂
a✝ : Integrable f₂
hf_eq : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
⊢ setToFun μ T hT g₂ = setToFun μ' T hT' g₂
have hfg' : f₂ =ᵐ[μ'] g₂ := (Measure.absolutelyContinuous_of_le_smul hμ'_le).ae_eq hfg
no goals
case h_ae
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1643104
G : Type ?u.1643107
𝕜 : Type ?u.1643110
p : ℝ≥0∞
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f✝ g : α → E
μ' : Measure α
c' : ℝ≥0∞
hc' : c' ≠ ⊤
hμ'_le : μ' ≤ c' • μ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ' T C'
f : α → E
hfμ : Integrable f
h_int : ∀ (g : α → E), Integrable g → Integrable g
f₂ g₂ : α → E
hfg : f₂ =ᵐ[μ] g₂
a✝ : Integrable f₂
hf_eq : setToFun μ T hT f₂ = setToFun μ' T hT' f₂
hfg' : f₂ =ᵐ[μ'] g₂
⊢ setToFun μ T hT g₂ = setToFun μ' T hT' g₂
rw [← setToFun_congr_ae hT hfg, hf_eq, setToFun_congr_ae hT' hfg']