[GOAL]
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → ℝ
h : Memℒp f 2
⊢ Integrable fun x => f x ^ 2
[PROOFSTEP]
simpa [← memℒp_one_iff_integrable] using h.norm_rpow two_ne_zero ENNReal.two_ne_top
[GOAL]
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ Memℒp f 2 ↔ Integrable fun x => ‖f x‖ ^ 2
[PROOFSTEP]
rw [← memℒp_one_iff_integrable]
[GOAL]
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ Memℒp f 2 ↔ Memℒp (fun x => ‖f x‖ ^ 2) 1
[PROOFSTEP]
convert (memℒp_norm_rpow_iff hf two_ne_zero ENNReal.two_ne_top).symm
[GOAL]
case h.e'_2.h.e'_5.h
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
x✝ : α
⊢ ‖f x✝‖ ^ 2 = ‖f x✝‖ ^ ENNReal.toReal 2
[PROOFSTEP]
simp
[GOAL]
case h.e'_2.h.e'_6
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
hf : AEStronglyMeasurable f μ
⊢ 1 = 2 / 2
[PROOFSTEP]
rw [div_eq_mul_inv, ENNReal.mul_inv_cancel two_ne_zero ENNReal.two_ne_top]
[GOAL]
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → ℝ
hf : AEStronglyMeasurable f μ
⊢ Memℒp f 2 ↔ Integrable fun x => f x ^ 2
[PROOFSTEP]
convert memℒp_two_iff_integrable_sq_norm hf using 3
[GOAL]
case h.e'_2.h.e'_5.h
α : Type u_1
F : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → ℝ
hf : AEStronglyMeasurable f μ
x✝ : α
⊢ f x✝ ^ 2 = ‖f x✝‖ ^ 2
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
hf : Memℒp f p
c : E
x : α
⊢ ‖inner (f x) c‖ ≤ ?m.29677 hf c * ‖f x‖
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
hf : Memℒp f p
c : E
x : α
⊢ ‖inner (f x) c‖ ≤ ‖f x‖ * ?m.29677 hf c
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ {f : α → E} → Memℒp f p → E → ℝ
[PROOFSTEP]
exact norm_inner_le_norm _ _
[GOAL]
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
c : E
hf : Integrable f
⊢ Integrable fun x => inner c (f x)
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at hf ⊢
[GOAL]
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
c : E
hf : Memℒp f 1
⊢ Memℒp (fun x => inner c (f x)) 1
[PROOFSTEP]
exact hf.const_inner c
[GOAL]
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
hf : Integrable f
c : E
⊢ Integrable fun x => inner (f x) c
[PROOFSTEP]
rw [← memℒp_one_iff_integrable] at hf ⊢
[GOAL]
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
hf : Memℒp f 1
c : E
⊢ Memℒp (fun x => inner (f x) c) 1
[PROOFSTEP]
exact hf.inner_const c
[GOAL]
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
f✝ : α → E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f
hf_int : ∀ (c : E), ∫ (x : α), inner c (f x) ∂μ = 0
⊢ ∫ (x : α), f x ∂μ = 0
[PROOFSTEP]
specialize hf_int (∫ x, f x ∂μ)
[GOAL]
α : Type u_1
m : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
f✝ : α → E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f
hf_int : ∫ (x : α), inner (∫ (x : α), f x ∂μ) (f x) ∂μ = 0
⊢ ∫ (x : α), f x ∂μ = 0
[PROOFSTEP]
rwa [integral_inner hf, inner_self_eq_zero] at hf_int
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp F 2 }
⊢ snorm (fun x => ‖↑↑f x‖ ^ 2) 1 μ < ⊤
[PROOFSTEP]
have h_two : ENNReal.ofReal (2 : ℝ) = 2 := by simp [zero_le_one]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp F 2 }
⊢ ENNReal.ofReal 2 = 2
[PROOFSTEP]
simp [zero_le_one]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp F 2 }
h_two : ENNReal.ofReal 2 = 2
⊢ snorm (fun x => ‖↑↑f x‖ ^ 2) 1 μ < ⊤
[PROOFSTEP]
rw [snorm_norm_rpow f zero_lt_two, one_mul, h_two]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp F 2 }
h_two : ENNReal.ofReal 2 = 2
⊢ snorm (↑↑f) 2 μ ^ 2 < ⊤
[PROOFSTEP]
exact ENNReal.rpow_lt_top_of_nonneg zero_le_two (Lp.snorm_ne_top f)
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
⊢ snorm (fun x => inner (↑↑f x) (↑↑g x)) 1 μ < ⊤
[PROOFSTEP]
have h : ∀ x, ‖⟪f x, g x⟫‖ ≤ ‖‖f x‖ ^ (2 : ℝ) + ‖g x‖ ^ (2 : ℝ)‖ :=
  by
  intro x
  rw [← @Nat.cast_two ℝ, Real.rpow_nat_cast, Real.rpow_nat_cast]
  calc
    ‖⟪f x, g x⟫‖ ≤ ‖f x‖ * ‖g x‖ := norm_inner_le_norm _ _
    _ ≤ 2 * ‖f x‖ * ‖g x‖ :=
      (mul_le_mul_of_nonneg_right (le_mul_of_one_le_left (norm_nonneg _) one_le_two) (norm_nonneg _))
    _ ≤ ‖‖f x‖ ^ 2 + ‖g x‖ ^ 2‖ := (two_mul_le_add_sq _ _).trans (le_abs_self _)
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
⊢ ∀ (x : α), ‖inner (↑↑f x) (↑↑g x)‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
x : α
⊢ ‖inner (↑↑f x) (↑↑g x)‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖
[PROOFSTEP]
rw [← @Nat.cast_two ℝ, Real.rpow_nat_cast, Real.rpow_nat_cast]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
x : α
⊢ ‖inner (↑↑f x) (↑↑g x)‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖
[PROOFSTEP]
calc
  ‖⟪f x, g x⟫‖ ≤ ‖f x‖ * ‖g x‖ := norm_inner_le_norm _ _
  _ ≤ 2 * ‖f x‖ * ‖g x‖ :=
    (mul_le_mul_of_nonneg_right (le_mul_of_one_le_left (norm_nonneg _) one_le_two) (norm_nonneg _))
  _ ≤ ‖‖f x‖ ^ 2 + ‖g x‖ ^ 2‖ := (two_mul_le_add_sq _ _).trans (le_abs_self _)
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
h : ∀ (x : α), ‖inner (↑↑f x) (↑↑g x)‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖
⊢ snorm (fun x => inner (↑↑f x) (↑↑g x)) 1 μ < ⊤
[PROOFSTEP]
refine' (snorm_mono_ae (ae_of_all _ h)).trans_lt ((snorm_add_le _ _ le_rfl).trans_lt _)
[GOAL]
case refine'_1
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
h : ∀ (x : α), ‖inner (↑↑f x) (↑↑g x)‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖
⊢ AEStronglyMeasurable (fun a => ‖↑↑f a‖ ^ 2) μ
[PROOFSTEP]
exact ((Lp.aestronglyMeasurable f).norm.aemeasurable.pow_const _).aestronglyMeasurable
[GOAL]
case refine'_2
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
h : ∀ (x : α), ‖inner (↑↑f x) (↑↑g x)‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖
⊢ AEStronglyMeasurable (fun a => ‖↑↑g a‖ ^ 2) μ
[PROOFSTEP]
exact ((Lp.aestronglyMeasurable g).norm.aemeasurable.pow_const _).aestronglyMeasurable
[GOAL]
case refine'_3
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
h : ∀ (x : α), ‖inner (↑↑f x) (↑↑g x)‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖
⊢ snorm (fun a => ‖↑↑f a‖ ^ 2) 1 μ + snorm (fun a => ‖↑↑g a‖ ^ 2) 1 μ < ⊤
[PROOFSTEP]
rw [ENNReal.add_lt_top]
[GOAL]
case refine'_3
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
h : ∀ (x : α), ‖inner (↑↑f x) (↑↑g x)‖ ≤ ‖‖↑↑f x‖ ^ 2 + ‖↑↑g x‖ ^ 2‖
⊢ snorm (fun a => ‖↑↑f a‖ ^ 2) 1 μ < ⊤ ∧ snorm (fun a => ‖↑↑g a‖ ^ 2) 1 μ < ⊤
[PROOFSTEP]
exact ⟨snorm_rpow_two_norm_lt_top f, snorm_rpow_two_norm_lt_top g⟩
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
⊢ ∫ (a : α), inner (↑↑f a) (↑↑f a) ∂μ = ↑(ENNReal.toReal (∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ))
[PROOFSTEP]
simp_rw [inner_self_eq_norm_sq_to_K]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
⊢ ∫ (a : α), ↑‖↑↑f a‖ ^ 2 ∂μ = ↑(ENNReal.toReal (∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ))
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
⊢ ∫ (a : α), ‖↑↑f a‖ ^ 2 ∂μ = ENNReal.toReal (∫⁻ (a : α), ↑(‖↑↑f a‖₊ ^ 2) ∂μ)
[PROOFSTEP]
rw [integral_eq_lintegral_of_nonneg_ae]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (‖↑↑f a‖ ^ 2) ∂μ) = ENNReal.toReal (∫⁻ (a : α), ↑(‖↑↑f a‖₊ ^ 2) ∂μ)
case hf
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
⊢ 0 ≤ᵐ[μ] fun a => ‖↑↑f a‖ ^ 2
case hfm
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
⊢ AEStronglyMeasurable (fun a => ‖↑↑f a‖ ^ 2) μ
[PROOFSTEP]
rotate_left
[GOAL]
case hf
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
⊢ 0 ≤ᵐ[μ] fun a => ‖↑↑f a‖ ^ 2
[PROOFSTEP]
exact Filter.eventually_of_forall fun x => sq_nonneg _
[GOAL]
case hfm
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
⊢ AEStronglyMeasurable (fun a => ‖↑↑f a‖ ^ 2) μ
[PROOFSTEP]
exact ((Lp.aestronglyMeasurable f).norm.aemeasurable.pow_const _).aestronglyMeasurable
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
⊢ ENNReal.toReal (∫⁻ (a : α), ENNReal.ofReal (‖↑↑f a‖ ^ 2) ∂μ) = ENNReal.toReal (∫⁻ (a : α), ↑(‖↑↑f a‖₊ ^ 2) ∂μ)
[PROOFSTEP]
congr
[GOAL]
case e_a.e_f
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
⊢ (fun a => ENNReal.ofReal (‖↑↑f a‖ ^ 2)) = fun a => ↑(‖↑↑f a‖₊ ^ 2)
[PROOFSTEP]
ext1 x
[GOAL]
case e_a.e_f.h
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
x : α
⊢ ENNReal.ofReal (‖↑↑f x‖ ^ 2) = ↑(‖↑↑f x‖₊ ^ 2)
[PROOFSTEP]
have h_two : (2 : ℝ) = ((2 : ℕ) : ℝ) := by simp
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
x : α
⊢ 2 = ↑2
[PROOFSTEP]
simp
[GOAL]
case e_a.e_f.h
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
x : α
h_two : 2 = ↑2
⊢ ENNReal.ofReal (‖↑↑f x‖ ^ 2) = ↑(‖↑↑f x‖₊ ^ 2)
[PROOFSTEP]
rw [← Real.rpow_nat_cast _ 2, ← h_two, ← ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) zero_le_two,
  ofReal_norm_eq_coe_nnnorm]
[GOAL]
case e_a.e_f.h
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
x : α
h_two : 2 = ↑2
⊢ ↑‖↑↑f x‖₊ ^ 2 = ↑(‖↑↑f x‖₊ ^ 2)
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
⊢ ‖f‖ ^ 2 = ↑IsROrC.re (inner f f)
[PROOFSTEP]
have h_two : (2 : ℝ≥0∞).toReal = 2 := by simp
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
⊢ ENNReal.toReal 2 = 2
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
h_two : ENNReal.toReal 2 = 2
⊢ ‖f‖ ^ 2 = ↑IsROrC.re (inner f f)
[PROOFSTEP]
rw [inner_def, integral_inner_eq_sq_snorm, norm_def, ← ENNReal.toReal_pow, IsROrC.ofReal_re,
  ENNReal.toReal_eq_toReal (ENNReal.pow_ne_top (Lp.snorm_ne_top f)) _]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
h_two : ENNReal.toReal 2 = 2
⊢ snorm (↑↑f) 2 μ ^ 2 = ∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ
[PROOFSTEP]
rw [← ENNReal.rpow_nat_cast, snorm_eq_snorm' two_ne_zero ENNReal.two_ne_top, snorm', ← ENNReal.rpow_mul, one_div, h_two]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
h_two : ENNReal.toReal 2 = 2
⊢ (∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ) ^ (2⁻¹ * ↑2) = ∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
h_two : ENNReal.toReal 2 = 2
⊢ ∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ ≠ ⊤
[PROOFSTEP]
refine' (lintegral_rpow_nnnorm_lt_top_of_snorm'_lt_top zero_lt_two _).ne
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
h_two : ENNReal.toReal 2 = 2
⊢ snorm' (fun a => ↑↑f a) 2 μ < ⊤
[PROOFSTEP]
rw [← h_two, ← snorm_eq_snorm' two_ne_zero ENNReal.two_ne_top]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f : { x // x ∈ Lp E 2 }
h_two : ENNReal.toReal 2 = 2
⊢ snorm (fun a => ↑↑f a) 2 μ < ⊤
[PROOFSTEP]
exact Lp.snorm_lt_top f
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
⊢ AEEqFun.mk (fun x => inner (↑↑f x) (↑↑g x)) (_ : AEStronglyMeasurable (fun x => inner (↑↑f x) (↑↑g x)) μ) ∈ Lp 𝕜 1
[PROOFSTEP]
simp_rw [mem_Lp_iff_snorm_lt_top, snorm_aeeqFun]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
⊢ snorm (fun x => inner (↑↑f x) (↑↑g x)) 1 μ < ⊤
[PROOFSTEP]
exact snorm_inner_lt_top f g
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f f' g : { x // x ∈ Lp E 2 }
⊢ inner (f + f') g = inner f g + inner f' g
[PROOFSTEP]
simp_rw [inner_def, ← integral_add (integrable_inner f g) (integrable_inner f' g), ← inner_add_left]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f f' g : { x // x ∈ Lp E 2 }
⊢ ∫ (a : α), inner (↑↑(f + f') a) (↑↑g a) ∂μ = ∫ (a : α), inner (↑↑f a + ↑↑f' a) (↑↑g a) ∂μ
[PROOFSTEP]
refine'
  integral_congr_ae
    ((coeFn_add f f').mono fun x hx => _)
      -- Porting note: was
        -- congr
        -- rwa [Pi.add_apply] at hx
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f f' g : { x // x ∈ Lp E 2 }
x : α
hx : ↑↑(f + f') x = (↑↑f + ↑↑f') x
⊢ (fun a => inner (↑↑(f + f') a) (↑↑g a)) x = (fun a => inner (↑↑f a + ↑↑f' a) (↑↑g a)) x
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f f' g : { x // x ∈ Lp E 2 }
x : α
hx : ↑↑(f + f') x = (↑↑f + ↑↑f') x
⊢ inner (↑↑(f + f') x) (↑↑g x) = inner (↑↑f x + ↑↑f' x) (↑↑g x)
[PROOFSTEP]
rw [hx, Pi.add_apply]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
r : 𝕜
⊢ inner (r • f) g = ↑(starRingEnd 𝕜) r * inner f g
[PROOFSTEP]
rw [inner_def, inner_def, ← smul_eq_mul, ← integral_smul]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
r : 𝕜
⊢ ∫ (a : α), inner (↑↑(r • f) a) (↑↑g a) ∂μ = ∫ (a : α), ↑(starRingEnd 𝕜) r • inner (↑↑f a) (↑↑g a) ∂μ
[PROOFSTEP]
refine' integral_congr_ae ((coeFn_smul r f).mono fun x hx => _)
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
r : 𝕜
x : α
hx : ↑↑(r • f) x = (r • ↑↑f) x
⊢ (fun a => inner (↑↑(r • f) a) (↑↑g a)) x = (fun a => ↑(starRingEnd 𝕜) r • inner (↑↑f a) (↑↑g a)) x
[PROOFSTEP]
simp only
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
f g : { x // x ∈ Lp E 2 }
r : 𝕜
x : α
hx : ↑↑(r • f) x = (r • ↑↑f) x
⊢ inner (↑↑(r • f) x) (↑↑g x) = ↑(starRingEnd 𝕜) r • inner (↑↑f x) (↑↑g x)
[PROOFSTEP]
rw [smul_eq_mul, ← inner_smul_left, hx, Pi.smul_apply]
  -- Porting note: was
    -- rw [smul_eq_mul, ← inner_smul_left]
    -- congr
    -- rwa [Pi.smul_apply] at hx
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
x✝¹ x✝ : { x // x ∈ Lp E 2 }
⊢ ↑(starRingEnd 𝕜) (inner x✝ x✝¹) = inner x✝¹ x✝
[PROOFSTEP]
simp_rw [inner_def, ← integral_conj, inner_conj_symm]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
⊢ inner (indicatorConstLp 2 hs hμs c) f = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
[PROOFSTEP]
rw [inner_def, ← integral_add_compl hs (L2.integrable_inner _ f)]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
⊢ ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ +
      ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ =
    ∫ (x : α) in s, inner c (↑↑f x) ∂μ
[PROOFSTEP]
have h_left : (∫ x in s, ⟪(indicatorConstLp 2 hs hμs c) x, f x⟫ ∂μ) = ∫ x in s, ⟪c, f x⟫ ∂μ :=
  by
  suffices h_ae_eq : ∀ᵐ x ∂μ, x ∈ s → ⟪indicatorConstLp 2 hs hμs c x, f x⟫ = ⟪c, f x⟫
  exact set_integral_congr_ae hs h_ae_eq
  have h_indicator : ∀ᵐ x : α ∂μ, x ∈ s → indicatorConstLp 2 hs hμs c x = c := indicatorConstLp_coeFn_mem
  refine' h_indicator.mono fun x hx hxs => _
  congr
  exact hx hxs
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
⊢ ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
[PROOFSTEP]
suffices h_ae_eq : ∀ᵐ x ∂μ, x ∈ s → ⟪indicatorConstLp 2 hs hμs c x, f x⟫ = ⟪c, f x⟫
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_ae_eq : ∀ᵐ (x : α) ∂μ, x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = inner c (↑↑f x)
⊢ ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = inner c (↑↑f x)
[PROOFSTEP]
exact set_integral_congr_ae hs h_ae_eq
[GOAL]
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = inner c (↑↑f x)
[PROOFSTEP]
have h_indicator : ∀ᵐ x : α ∂μ, x ∈ s → indicatorConstLp 2 hs hμs c x = c := indicatorConstLp_coeFn_mem
[GOAL]
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_indicator : ∀ᵐ (x : α) ∂μ, x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = c
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = inner c (↑↑f x)
[PROOFSTEP]
refine' h_indicator.mono fun x hx hxs => _
[GOAL]
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_indicator : ∀ᵐ (x : α) ∂μ, x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = c
x : α
hx : x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = c
hxs : x ∈ s
⊢ inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = inner c (↑↑f x)
[PROOFSTEP]
congr
[GOAL]
case h_ae_eq.e_a
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_indicator : ∀ᵐ (x : α) ∂μ, x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = c
x : α
hx : x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = c
hxs : x ∈ s
⊢ ↑↑(indicatorConstLp 2 hs hμs c) x = c
[PROOFSTEP]
exact hx hxs
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
⊢ ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ +
      ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ =
    ∫ (x : α) in s, inner c (↑↑f x) ∂μ
[PROOFSTEP]
have h_right : (∫ x in sᶜ, ⟪(indicatorConstLp 2 hs hμs c) x, f x⟫ ∂μ) = 0 :=
  by
  suffices h_ae_eq : ∀ᵐ x ∂μ, x ∉ s → ⟪indicatorConstLp 2 hs hμs c x, f x⟫ = 0
  · simp_rw [← Set.mem_compl_iff] at h_ae_eq
    suffices h_int_zero : (∫ x in sᶜ, inner (indicatorConstLp 2 hs hμs c x) (f x) ∂μ) = ∫ _ in sᶜ, (0 : 𝕜) ∂μ
    · rw [h_int_zero]
      simp
    exact set_integral_congr_ae hs.compl h_ae_eq
  have h_indicator : ∀ᵐ x : α ∂μ, x ∉ s → indicatorConstLp 2 hs hμs c x = 0 := indicatorConstLp_coeFn_nmem
  refine' h_indicator.mono fun x hx hxs => _
  rw [hx hxs]
  exact inner_zero_left _
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
⊢ ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = 0
[PROOFSTEP]
suffices h_ae_eq : ∀ᵐ x ∂μ, x ∉ s → ⟪indicatorConstLp 2 hs hμs c x, f x⟫ = 0
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_ae_eq : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
⊢ ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = 0
[PROOFSTEP]
simp_rw [← Set.mem_compl_iff] at h_ae_eq
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_ae_eq : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
⊢ ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = 0
[PROOFSTEP]
suffices h_int_zero : (∫ x in sᶜ, inner (indicatorConstLp 2 hs hμs c x) (f x) ∂μ) = ∫ _ in sᶜ, (0 : 𝕜) ∂μ
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_ae_eq : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
h_int_zero : ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in sᶜ, 0 ∂μ
⊢ ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = 0
[PROOFSTEP]
rw [h_int_zero]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_ae_eq : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
h_int_zero : ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in sᶜ, 0 ∂μ
⊢ ∫ (x : α) in sᶜ, 0 ∂μ = 0
[PROOFSTEP]
simp
[GOAL]
case h_int_zero
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_ae_eq : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
⊢ ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in sᶜ, 0 ∂μ
[PROOFSTEP]
exact set_integral_congr_ae hs.compl h_ae_eq
[GOAL]
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
⊢ ∀ᵐ (x : α) ∂μ, ¬x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
[PROOFSTEP]
have h_indicator : ∀ᵐ x : α ∂μ, x ∉ s → indicatorConstLp 2 hs hμs c x = 0 := indicatorConstLp_coeFn_nmem
[GOAL]
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_indicator : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
⊢ ∀ᵐ (x : α) ∂μ, ¬x ∈ s → inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
[PROOFSTEP]
refine' h_indicator.mono fun x hx hxs => _
[GOAL]
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_indicator : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
x : α
hx : ¬x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
hxs : ¬x ∈ s
⊢ inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) = 0
[PROOFSTEP]
rw [hx hxs]
[GOAL]
case h_ae_eq
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_indicator : ∀ᵐ (x : α) ∂μ, ¬x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
x : α
hx : ¬x ∈ s → ↑↑(indicatorConstLp 2 hs hμs c) x = 0
hxs : ¬x ∈ s
⊢ inner 0 (↑↑f x) = 0
[PROOFSTEP]
exact inner_zero_left _
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
f : { x // x ∈ Lp E 2 }
hs : MeasurableSet s
c : E
hμs : ↑↑μ s ≠ ⊤
h_left : ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = ∫ (x : α) in s, inner c (↑↑f x) ∂μ
h_right : ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ = 0
⊢ ∫ (x : α) in s, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ +
      ∫ (x : α) in sᶜ, inner (↑↑(indicatorConstLp 2 hs hμs c) x) (↑↑f x) ∂μ =
    ∫ (x : α) in s, inner c (↑↑f x) ∂μ
[PROOFSTEP]
rw [h_left, h_right, add_zero]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : MeasurableSpace α
μ : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
s : Set α
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
c : E
f : { x // x ∈ Lp E 2 }
⊢ inner (indicatorConstLp 2 hs hμs c) f = inner c (∫ (x : α) in s, ↑↑f x ∂μ)
[PROOFSTEP]
rw [← integral_inner (integrableOn_Lp_of_measure_ne_top f fact_one_le_two_ennreal.elim hμs),
  L2.inner_indicatorConstLp_eq_set_integral_inner]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
f : { x // x ∈ Lp 𝕜 2 }
⊢ inner (indicatorConstLp 2 hs hμs 1) f = ∫ (x : α) in s, ↑↑f x ∂μ
[PROOFSTEP]
rw [L2.inner_indicatorConstLp_eq_inner_set_integral 𝕜 hs hμs (1 : 𝕜) f]
[GOAL]
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : NormedAddCommGroup F
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
f : { x // x ∈ Lp 𝕜 2 }
⊢ inner 1 (∫ (x : α) in s, ↑↑f x ∂μ) = ∫ (x : α) in s, ↑↑f x ∂μ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasureSpace α
inst✝² : BorelSpace α
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
⊢ inner (↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) (↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) =
    ∫ (x : α), ↑(starRingEnd ((fun a => 𝕜) x)) (↑f x) * ↑g x ∂μ
[PROOFSTEP]
apply integral_congr_ae
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasureSpace α
inst✝² : BorelSpace α
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
⊢ (fun a =>
      inner (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) a) (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) a)) =ᵐ[μ]
    fun a => ↑(starRingEnd ((fun a => 𝕜) a)) (↑f a) * ↑g a
[PROOFSTEP]
have hf_ae := f.coeFn_toLp 2 μ 𝕜
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasureSpace α
inst✝² : BorelSpace α
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᵐ[μ] ↑f
⊢ (fun a =>
      inner (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) a) (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) a)) =ᵐ[μ]
    fun a => ↑(starRingEnd ((fun a => 𝕜) a)) (↑f a) * ↑g a
[PROOFSTEP]
have hg_ae := g.coeFn_toLp 2 μ 𝕜
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasureSpace α
inst✝² : BorelSpace α
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᵐ[μ] ↑f
hg_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) =ᵐ[μ] ↑g
⊢ (fun a =>
      inner (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) a) (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) a)) =ᵐ[μ]
    fun a => ↑(starRingEnd ((fun a => 𝕜) a)) (↑f a) * ↑g a
[PROOFSTEP]
filter_upwards [hf_ae, hg_ae] with _ hf hg
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasureSpace α
inst✝² : BorelSpace α
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᵐ[μ] ↑f
hg_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) =ᵐ[μ] ↑g
a✝ : α
hf : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) a✝ = ↑f a✝
hg : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) a✝ = ↑g a✝
⊢ inner (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) a✝) (↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) a✝) =
    ↑(starRingEnd 𝕜) (↑f a✝) * ↑g a✝
[PROOFSTEP]
rw [hf, hg]
[GOAL]
case h
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : MeasureSpace α
inst✝² : BorelSpace α
𝕜 : Type u_2
inst✝¹ : IsROrC 𝕜
μ : Measure α
inst✝ : IsFiniteMeasure μ
f g : α →ᵇ 𝕜
hf_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᵐ[μ] ↑f
hg_ae : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) =ᵐ[μ] ↑g
a✝ : α
hf : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) f) a✝ = ↑f a✝
hg : ↑↑(↑(BoundedContinuousFunction.toLp 2 μ 𝕜) g) a✝ = ↑g a✝
⊢ inner (↑f a✝) (↑g a✝) = ↑(starRingEnd 𝕜) (↑f a✝) * ↑g a✝
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasureSpace α
inst✝³ : BorelSpace α
𝕜 : Type u_2
inst✝² : IsROrC 𝕜
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
⊢ inner (↑(ContinuousMap.toLp 2 μ 𝕜) f) (↑(ContinuousMap.toLp 2 μ 𝕜) g) =
    ∫ (x : α), ↑(starRingEnd ((fun x => 𝕜) x)) (↑f x) * ↑g x ∂μ
[PROOFSTEP]
apply integral_congr_ae
[GOAL]
case h
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasureSpace α
inst✝³ : BorelSpace α
𝕜 : Type u_2
inst✝² : IsROrC 𝕜
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
⊢ (fun a => inner (↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) f) a) (↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) g) a)) =ᵐ[μ] fun a =>
    ↑(starRingEnd ((fun x => 𝕜) a)) (↑f a) * ↑g a
[PROOFSTEP]
have hf_ae := f.coeFn_toLp (p := 2) (𝕜 := 𝕜) μ
[GOAL]
case h
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasureSpace α
inst✝³ : BorelSpace α
𝕜 : Type u_2
inst✝² : IsROrC 𝕜
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
hf_ae : ↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) f) =ᵐ[μ] ↑f
⊢ (fun a => inner (↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) f) a) (↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) g) a)) =ᵐ[μ] fun a =>
    ↑(starRingEnd ((fun x => 𝕜) a)) (↑f a) * ↑g a
[PROOFSTEP]
have hg_ae := g.coeFn_toLp (p := 2) (𝕜 := 𝕜) μ
[GOAL]
case h
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasureSpace α
inst✝³ : BorelSpace α
𝕜 : Type u_2
inst✝² : IsROrC 𝕜
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
hf_ae : ↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) f) =ᵐ[μ] ↑f
hg_ae : ↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) g) =ᵐ[μ] ↑g
⊢ (fun a => inner (↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) f) a) (↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) g) a)) =ᵐ[μ] fun a =>
    ↑(starRingEnd ((fun x => 𝕜) a)) (↑f a) * ↑g a
[PROOFSTEP]
filter_upwards [hf_ae, hg_ae] with _ hf hg
[GOAL]
case h
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasureSpace α
inst✝³ : BorelSpace α
𝕜 : Type u_2
inst✝² : IsROrC 𝕜
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
hf_ae : ↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) f) =ᵐ[μ] ↑f
hg_ae : ↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) g) =ᵐ[μ] ↑g
a✝ : α
hf : ↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) f) a✝ = ↑f a✝
hg : ↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) g) a✝ = ↑g a✝
⊢ inner (↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) f) a✝) (↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) g) a✝) = ↑(starRingEnd 𝕜) (↑f a✝) * ↑g a✝
[PROOFSTEP]
rw [hf, hg]
[GOAL]
case h
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : MeasureSpace α
inst✝³ : BorelSpace α
𝕜 : Type u_2
inst✝² : IsROrC 𝕜
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : CompactSpace α
f g : C(α, 𝕜)
hf_ae : ↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) f) =ᵐ[μ] ↑f
hg_ae : ↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) g) =ᵐ[μ] ↑g
a✝ : α
hf : ↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) f) a✝ = ↑f a✝
hg : ↑↑(↑(ContinuousMap.toLp 2 μ 𝕜) g) a✝ = ↑g a✝
⊢ inner (↑f a✝) (↑g a✝) = ↑(starRingEnd 𝕜) (↑f a✝) * ↑g a✝
[PROOFSTEP]
simp


[GOAL]
a✝ : (Quotient.out (ord (aleph 1))).α
i : (Quotient.out (ord (aleph 1))).α := a✝
j : ↑(Iio i)
⊢ (invImage (fun a => a) (hasWellFoundedOut (ord (aleph 1)))).1 (↑j) a✝
[PROOFSTEP]
exact j.2
[GOAL]
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ s ⊆ generateMeasurableRec s i
[PROOFSTEP]
unfold generateMeasurableRec
[GOAL]
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ s ⊆
    let i := i;
    let S := ⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j;
    s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ (n : ℕ), ↑(f n)
[PROOFSTEP]
apply_rules [subset_union_of_subset_left]
[GOAL]
case h.h.h
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ s ⊆ s
[PROOFSTEP]
exact subset_rfl
[GOAL]
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ ∅ ∈ generateMeasurableRec s i
[PROOFSTEP]
unfold generateMeasurableRec
[GOAL]
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ ∅ ∈
    let i := i;
    let S := ⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j;
    s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ (n : ℕ), ↑(f n)
[PROOFSTEP]
exact mem_union_left _ (mem_union_left _ (mem_union_right _ (mem_singleton ∅)))
[GOAL]
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
h : j < i
t : Set α
ht : t ∈ generateMeasurableRec s j
⊢ tᶜ ∈ generateMeasurableRec s i
[PROOFSTEP]
unfold generateMeasurableRec
[GOAL]
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
h : j < i
t : Set α
ht : t ∈ generateMeasurableRec s j
⊢ tᶜ ∈
    let i := i;
    let S := ⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j;
    s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ (n : ℕ), ↑(f n)
[PROOFSTEP]
exact mem_union_left _ (mem_union_right _ ⟨t, mem_iUnion.2 ⟨⟨j, h⟩, ht⟩, rfl⟩)
[GOAL]
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
hf : ∀ (n : ℕ), ∃ j, j < i ∧ f n ∈ generateMeasurableRec s j
⊢ ⋃ (n : ℕ), f n ∈ generateMeasurableRec s i
[PROOFSTEP]
unfold generateMeasurableRec
[GOAL]
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
hf : ∀ (n : ℕ), ∃ j, j < i ∧ f n ∈ generateMeasurableRec s j
⊢ ⋃ (n : ℕ), f n ∈
    let i := i;
    let S := ⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j;
    s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ (n : ℕ), ↑(f n)
[PROOFSTEP]
exact
  mem_union_right _
    ⟨fun n =>
      ⟨f n,
        let ⟨j, hj, hf⟩ := hf n;
        mem_iUnion.2 ⟨⟨j, hj⟩, hf⟩⟩,
      rfl⟩
[GOAL]
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
h : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
⊢ x ∈ generateMeasurableRec s j
[PROOFSTEP]
rcases eq_or_lt_of_le h with (rfl | h)
[GOAL]
case inl
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i ≤ i
⊢ x ∈ generateMeasurableRec s i
[PROOFSTEP]
exact hx
[GOAL]
case inr
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
h✝ : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i < j
⊢ x ∈ generateMeasurableRec s j
[PROOFSTEP]
convert iUnion_mem_generateMeasurableRec fun _ => ⟨i, h, hx⟩
[GOAL]
case h.e'_4
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
h✝ : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i < j
⊢ x = ⋃ (n : ℕ), x
[PROOFSTEP]
exact (iUnion_const x).symm
[GOAL]
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
apply (aleph 1).ord.out.wo.wf.induction i
[GOAL]
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ ∀ (x : (Quotient.out (ord (aleph 1))).α),
    (∀ (y : (Quotient.out (ord (aleph 1))).α),
        WellOrder.r (Quotient.out (ord (aleph 1))) y x → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀) →
      #↑(generateMeasurableRec s x) ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
intro i IH
[GOAL]
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
⊢ #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
have A := aleph0_le_aleph 1
[GOAL]
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
⊢ #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
have B : aleph 1 ≤ max (#s) 2 ^ aleph0.{u} := aleph_one_le_continuum.trans (power_le_power_right (le_max_right _ _))
[GOAL]
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
⊢ #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
have C : ℵ₀ ≤ max (#s) 2 ^ aleph0.{u} := A.trans B
[GOAL]
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
⊢ #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
have J : #(⋃ j : Iio i, generateMeasurableRec s j.1) ≤ max (#s) 2 ^ aleph0.{u} :=
  by
  refine (mk_iUnion_le _).trans ?_
  have D : ⨆ j : Iio i, #(generateMeasurableRec s j) ≤ _ := ciSup_le' fun ⟨j, hj⟩ => IH j hj
  apply (mul_le_mul' ((mk_subtype_le _).trans (aleph 1).mk_ord_out.le) D).trans
  rw [mul_eq_max A C]
  exact max_le B le_rfl
[GOAL]
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
⊢ #↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j) ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
refine (mk_iUnion_le _).trans ?_
[GOAL]
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
⊢ #↑(Iio i) * ⨆ (i_1 : ↑(Iio i)), #↑(generateMeasurableRec s ↑i_1) ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
have D : ⨆ j : Iio i, #(generateMeasurableRec s j) ≤ _ := ciSup_le' fun ⟨j, hj⟩ => IH j hj
[GOAL]
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
D : ⨆ (j : ↑(Iio i)), #↑(generateMeasurableRec s ↑j) ≤ max (#↑s) 2 ^ ℵ₀
⊢ #↑(Iio i) * ⨆ (i_1 : ↑(Iio i)), #↑(generateMeasurableRec s ↑i_1) ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
apply (mul_le_mul' ((mk_subtype_le _).trans (aleph 1).mk_ord_out.le) D).trans
[GOAL]
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
D : ⨆ (j : ↑(Iio i)), #↑(generateMeasurableRec s ↑j) ≤ max (#↑s) 2 ^ ℵ₀
⊢ aleph 1 * max (#↑s) 2 ^ ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
rw [mul_eq_max A C]
[GOAL]
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
D : ⨆ (j : ↑(Iio i)), #↑(generateMeasurableRec s ↑j) ≤ max (#↑s) 2 ^ ℵ₀
⊢ max (aleph 1) (max (#↑s) 2 ^ ℵ₀) ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
exact max_le B le_rfl
[GOAL]
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : #↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j) ≤ max (#↑s) 2 ^ ℵ₀
⊢ #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
rw [generateMeasurableRec]
[GOAL]
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : #↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j) ≤ max (#↑s) 2 ^ ℵ₀
⊢ #↑((s ∪ {∅} ∪ compl '' ⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j) ∪ range fun f => ⋃ (n : ℕ), ↑(f n)) ≤
    max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
apply_rules [(mk_union_le _ _).trans, add_le_of_le C, mk_image_le.trans]
[GOAL]
case h1.h1.h1
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : #↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j) ≤ max (#↑s) 2 ^ ℵ₀
⊢ #↑s ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
exact (le_max_left _ _).trans (self_le_power _ one_lt_aleph0.le)
[GOAL]
case h1.h1.h2
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : #↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j) ≤ max (#↑s) 2 ^ ℵ₀
⊢ #↑{∅} ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
rw [mk_singleton]
[GOAL]
case h1.h1.h2
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : #↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j) ≤ max (#↑s) 2 ^ ℵ₀
⊢ 1 ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
exact one_lt_aleph0.le.trans C
[GOAL]
case h2
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : #↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j) ≤ max (#↑s) 2 ^ ℵ₀
⊢ #↑(range fun f => ⋃ (n : ℕ), ↑(f n)) ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
apply mk_range_le.trans
[GOAL]
case h2
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : #↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j) ≤ max (#↑s) 2 ^ ℵ₀
⊢ #(ℕ → ↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j)) ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
simp only [mk_pi, prod_const, lift_uzero, mk_denumerable, lift_aleph0]
[GOAL]
case h2
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : #↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j) ≤ max (#↑s) 2 ^ ℵ₀
⊢ #↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j) ^ ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
have := @power_le_power_right _ _ ℵ₀ J
[GOAL]
case h2
α : Type u
s : Set (Set α)
i✝ i : (Quotient.out (ord (aleph 1))).α
IH :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y i → #↑(generateMeasurableRec s y) ≤ max (#↑s) 2 ^ ℵ₀
A : ℵ₀ ≤ aleph 1
B : aleph 1 ≤ max (#↑s) 2 ^ ℵ₀
C : ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
J : #↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j) ≤ max (#↑s) 2 ^ ℵ₀
this : #↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j) ^ ℵ₀ ≤ (max (#↑s) 2 ^ ℵ₀) ^ ℵ₀
⊢ #↑(⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j) ^ ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
rwa [← power_mul, aleph0_mul_aleph0] at this
[GOAL]
α : Type u
s : Set (Set α)
⊢ {t | GenerateMeasurable s t} = ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
[PROOFSTEP]
ext t
[GOAL]
case h
α : Type u
s : Set (Set α)
t : Set α
⊢ t ∈ {t | GenerateMeasurable s t} ↔ t ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
[PROOFSTEP]
refine' ⟨fun ht => _, fun ht => _⟩
[GOAL]
case h.refine'_1
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ {t | GenerateMeasurable s t}
⊢ t ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
[PROOFSTEP]
inhabit ω₁
[GOAL]
case h.refine'_1
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ {t | GenerateMeasurable s t}
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
⊢ t ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
[PROOFSTEP]
induction' ht with u hu u _ IH f _ IH
[GOAL]
case h.refine'_1.basic
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
u : Set α
hu : u ∈ s
⊢ u ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
[PROOFSTEP]
exact mem_iUnion.2 ⟨default, self_subset_generateMeasurableRec s _ hu⟩
[GOAL]
case h.refine'_1.empty
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
⊢ ∅ ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
[PROOFSTEP]
exact mem_iUnion.2 ⟨default, empty_mem_generateMeasurableRec s _⟩
[GOAL]
case h.refine'_1.compl
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
u : Set α
a✝ : GenerateMeasurable s u
IH : u ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
⊢ uᶜ ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
[PROOFSTEP]
rcases mem_iUnion.1 IH with ⟨i, hi⟩
[GOAL]
case h.refine'_1.compl.intro
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
u : Set α
a✝ : GenerateMeasurable s u
IH : u ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
i : (Quotient.out (ord (aleph 1))).α
hi : u ∈ generateMeasurableRec s i
⊢ uᶜ ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
[PROOFSTEP]
obtain ⟨j, hj⟩ := exists_gt i
[GOAL]
case h.refine'_1.compl.intro.intro
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
u : Set α
a✝ : GenerateMeasurable s u
IH : u ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
i : (Quotient.out (ord (aleph 1))).α
hi : u ∈ generateMeasurableRec s i
j : (Quotient.out (ord (aleph 1))).α
hj : i < j
⊢ uᶜ ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
[PROOFSTEP]
exact mem_iUnion.2 ⟨j, compl_mem_generateMeasurableRec hj hi⟩
[GOAL]
case h.refine'_1.iUnion
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
⊢ ⋃ (i : ℕ), f i ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
[PROOFSTEP]
have : ∀ n, ∃ i, f n ∈ generateMeasurableRec s i := fun n => by simpa using IH n
[GOAL]
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
n : ℕ
⊢ ∃ i, f n ∈ generateMeasurableRec s i
[PROOFSTEP]
simpa using IH n
[GOAL]
case h.refine'_1.iUnion
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
this : ∀ (n : ℕ), ∃ i, f n ∈ generateMeasurableRec s i
⊢ ⋃ (i : ℕ), f i ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
[PROOFSTEP]
choose I hI using this
[GOAL]
case h.refine'_1.iUnion
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
I : ℕ → (Quotient.out (ord (aleph 1))).α
hI : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (I n)
⊢ ⋃ (i : ℕ), f i ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
[PROOFSTEP]
have : IsWellOrder (ω₁ : Type u) (· < ·) := isWellOrder_out_lt _
[GOAL]
case h.refine'_1.iUnion
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
I : ℕ → (Quotient.out (ord (aleph 1))).α
hI : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (I n)
this : IsWellOrder (Quotient.out (ord (aleph 1))).α fun x x_1 => x < x_1
⊢ ⋃ (i : ℕ), f i ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
[PROOFSTEP]
refine'
  mem_iUnion.2
    ⟨Ordinal.enum (· < ·) (Ordinal.lsub fun n => Ordinal.typein.{u} (· < ·) (I n)) _,
      iUnion_mem_generateMeasurableRec fun n => ⟨I n, _, hI n⟩⟩
[GOAL]
case h.refine'_1.iUnion.refine'_1
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
I : ℕ → (Quotient.out (ord (aleph 1))).α
hI : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (I n)
this : IsWellOrder (Quotient.out (ord (aleph 1))).α fun x x_1 => x < x_1
⊢ (Ordinal.lsub fun n => Ordinal.typein (fun x x_1 => x < x_1) (I n)) < Ordinal.type fun x x_1 => x < x_1
[PROOFSTEP]
rw [Ordinal.type_lt]
[GOAL]
case h.refine'_1.iUnion.refine'_1
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
I : ℕ → (Quotient.out (ord (aleph 1))).α
hI : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (I n)
this : IsWellOrder (Quotient.out (ord (aleph 1))).α fun x x_1 => x < x_1
⊢ (Ordinal.lsub fun n => Ordinal.typein (fun x x_1 => x < x_1) (I n)) < ord (aleph 1)
[PROOFSTEP]
refine' Ordinal.lsub_lt_ord_lift _ fun i => Ordinal.typein_lt_self _
[GOAL]
case h.refine'_1.iUnion.refine'_1
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
I : ℕ → (Quotient.out (ord (aleph 1))).α
hI : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (I n)
this : IsWellOrder (Quotient.out (ord (aleph 1))).α fun x x_1 => x < x_1
⊢ lift #ℕ < Ordinal.cof (ord (aleph 1))
[PROOFSTEP]
rw [mk_denumerable, lift_aleph0, isRegular_aleph_one.cof_eq]
[GOAL]
case h.refine'_1.iUnion.refine'_1
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
I : ℕ → (Quotient.out (ord (aleph 1))).α
hI : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (I n)
this : IsWellOrder (Quotient.out (ord (aleph 1))).α fun x x_1 => x < x_1
⊢ ℵ₀ < aleph 1
[PROOFSTEP]
exact aleph0_lt_aleph_one
[GOAL]
case h.refine'_1.iUnion.refine'_2
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
I : ℕ → (Quotient.out (ord (aleph 1))).α
hI : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (I n)
this : IsWellOrder (Quotient.out (ord (aleph 1))).α fun x x_1 => x < x_1
n : ℕ
⊢ I n <
    Ordinal.enum (fun x x_1 => x < x_1) (Ordinal.lsub fun n => Ordinal.typein (fun x x_1 => x < x_1) (I n))
      (_ : (Ordinal.lsub fun n => Ordinal.typein (fun x x_1 => x < x_1) (I n)) < Ordinal.type fun x x_1 => x < x_1)
[PROOFSTEP]
rw [← Ordinal.typein_lt_typein (· < ·), Ordinal.typein_enum]
[GOAL]
case h.refine'_1.iUnion.refine'_2
α : Type u
s : Set (Set α)
t : Set α
inhabited_h : Inhabited (Quotient.out (ord (aleph 1))).α
f : ℕ → Set α
a✝ : ∀ (n : ℕ), GenerateMeasurable s (f n)
IH : ∀ (n : ℕ), f n ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
I : ℕ → (Quotient.out (ord (aleph 1))).α
hI : ∀ (n : ℕ), f n ∈ generateMeasurableRec s (I n)
this : IsWellOrder (Quotient.out (ord (aleph 1))).α fun x x_1 => x < x_1
n : ℕ
⊢ Ordinal.typein (fun x x_1 => x < x_1) (I n) < Ordinal.lsub fun n => Ordinal.typein (fun x x_1 => x < x_1) (I n)
[PROOFSTEP]
apply Ordinal.lt_lsub fun n : ℕ => _
[GOAL]
case h.refine'_2
α : Type u
s : Set (Set α)
t : Set α
ht : t ∈ ⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i
⊢ t ∈ {t | GenerateMeasurable s t}
[PROOFSTEP]
rcases ht with ⟨t, ⟨i, rfl⟩, hx⟩
[GOAL]
case h.refine'_2.intro.intro.intro
α : Type u
s : Set (Set α)
t : Set α
i : (Quotient.out (ord (aleph 1))).α
hx : t ∈ (fun i => generateMeasurableRec s i) i
⊢ t ∈ {t | GenerateMeasurable s t}
[PROOFSTEP]
revert t
[GOAL]
case h.refine'_2.intro.intro.intro
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) i → t ∈ {t | GenerateMeasurable s t}
[PROOFSTEP]
apply (aleph 1).ord.out.wo.wf.induction i
[GOAL]
case h.refine'_2.intro.intro.intro
α : Type u
s : Set (Set α)
i : (Quotient.out (ord (aleph 1))).α
⊢ ∀ (x : (Quotient.out (ord (aleph 1))).α),
    (∀ (y : (Quotient.out (ord (aleph 1))).α),
        WellOrder.r (Quotient.out (ord (aleph 1))) y x →
          ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}) →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) x → t ∈ {t | GenerateMeasurable s t}
[PROOFSTEP]
intro j H t ht
[GOAL]
case h.refine'_2.intro.intro.intro
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
t : Set α
ht : t ∈ (fun i => generateMeasurableRec s i) j
⊢ t ∈ {t | GenerateMeasurable s t}
[PROOFSTEP]
unfold generateMeasurableRec at ht
[GOAL]
case h.refine'_2.intro.intro.intro
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
t : Set α
ht :
  t ∈
    let i := j;
    let S := ⋃ (j : ↑(Iio i)), generateMeasurableRec s ↑j;
    s ∪ {∅} ∪ compl '' S ∪ range fun f => ⋃ (n : ℕ), ↑(f n)
⊢ t ∈ {t | GenerateMeasurable s t}
[PROOFSTEP]
rcases ht with (((h | (rfl : t = ∅)) | ⟨u, ⟨-, ⟨⟨k, hk⟩, rfl⟩, hu⟩, rfl⟩) | ⟨f, rfl⟩)
[GOAL]
case h.refine'_2.intro.intro.intro.inl.inl.inl
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
t : Set α
h : t ∈ s
⊢ t ∈ {t | GenerateMeasurable s t}
[PROOFSTEP]
exact .basic t h
[GOAL]
case h.refine'_2.intro.intro.intro.inl.inl.inr
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
⊢ ∅ ∈ {t | GenerateMeasurable s t}
[PROOFSTEP]
exact .empty
[GOAL]
case h.refine'_2.intro.intro.intro.inl.inr.intro.intro.intro.intro.intro.mk
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
u : Set α
k : (Quotient.out (ord (aleph 1))).α
hk : k ∈ Iio j
hu : u ∈ (fun j_1 => generateMeasurableRec s ↑j_1) { val := k, property := hk }
⊢ uᶜ ∈ {t | GenerateMeasurable s t}
[PROOFSTEP]
exact .compl u (H k hk u hu)
[GOAL]
case h.refine'_2.intro.intro.intro.inr.intro
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
f : ℕ → ↑(⋃ (j_1 : ↑(Iio j)), generateMeasurableRec s ↑j_1)
⊢ (fun f => ⋃ (n : ℕ), ↑(f n)) f ∈ {t | GenerateMeasurable s t}
[PROOFSTEP]
refine .iUnion _ @fun n => ?_
[GOAL]
case h.refine'_2.intro.intro.intro.inr.intro
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
f : ℕ → ↑(⋃ (j_1 : ↑(Iio j)), generateMeasurableRec s ↑j_1)
n : ℕ
⊢ GenerateMeasurable s ↑(f n)
[PROOFSTEP]
obtain ⟨-, ⟨⟨k, hk⟩, rfl⟩, hf⟩ := (f n).prop
[GOAL]
case h.refine'_2.intro.intro.intro.inr.intro.intro.intro.intro.mk
α : Type u
s : Set (Set α)
i j : (Quotient.out (ord (aleph 1))).α
H :
  ∀ (y : (Quotient.out (ord (aleph 1))).α),
    WellOrder.r (Quotient.out (ord (aleph 1))) y j →
      ∀ (t : Set α), t ∈ (fun i => generateMeasurableRec s i) y → t ∈ {t | GenerateMeasurable s t}
f : ℕ → ↑(⋃ (j_1 : ↑(Iio j)), generateMeasurableRec s ↑j_1)
n : ℕ
k : (Quotient.out (ord (aleph 1))).α
hk : k ∈ Iio j
hf : ↑(f n) ∈ (fun j_1 => generateMeasurableRec s ↑j_1) { val := k, property := hk }
⊢ GenerateMeasurable s ↑(f n)
[PROOFSTEP]
exact H k hk _ hf
[GOAL]
α : Type u
s : Set (Set α)
⊢ #↑{t | GenerateMeasurable s t} ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
rw [generateMeasurable_eq_rec]
[GOAL]
α : Type u
s : Set (Set α)
⊢ #↑(⋃ (i : (Quotient.out (ord (aleph 1))).α), generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
apply (mk_iUnion_le _).trans
[GOAL]
α : Type u
s : Set (Set α)
⊢ #(Quotient.out (ord (aleph 1))).α * ⨆ (i : (Quotient.out (ord (aleph 1))).α), #↑(generateMeasurableRec s i) ≤
    max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
rw [(aleph 1).mk_ord_out]
[GOAL]
α : Type u
s : Set (Set α)
⊢ aleph 1 * ⨆ (i : (Quotient.out (ord (aleph 1))).α), #↑(generateMeasurableRec s i) ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
refine le_trans (mul_le_mul' aleph_one_le_continuum (ciSup_le' fun i => cardinal_generateMeasurableRec_le s i)) ?_
[GOAL]
α : Type u
s : Set (Set α)
⊢ 𝔠 * max (#↑s) 2 ^ ℵ₀ ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
refine (mul_le_max_of_aleph0_le_left aleph0_le_continuum).trans (max_le ?_ le_rfl)
[GOAL]
α : Type u
s : Set (Set α)
⊢ 𝔠 ≤ max (#↑s) 2 ^ ℵ₀
[PROOFSTEP]
exact power_le_power_right (le_max_right _ _)
[GOAL]
α : Type u
s : Set (Set α)
hs : #↑s ≤ 𝔠
⊢ max (#↑s) 2 ^ ℵ₀ ≤ 𝔠
[PROOFSTEP]
rw [← continuum_power_aleph0]
[GOAL]
α : Type u
s : Set (Set α)
hs : #↑s ≤ 𝔠
⊢ max (#↑s) 2 ^ ℵ₀ ≤ 𝔠 ^ ℵ₀
[PROOFSTEP]
exact_mod_cast power_le_power_right (max_le hs (nat_lt_continuum 2).le)