-- Mathlib/Probability/Independence/Integrable.lean
/-- If a nonzero function belongs to `ℒ^p` and is independent of another function, then
the space is a probability space. -/
lemma MemLp.isProbabilityMeasure_of_indepFun
    (f : Ω → E) (g : Ω → F) {p : ℝ≥0∞} (hp : p ≠ 0) (hp' : p ≠ ∞)
    (hℒp : MemLp f p μ) (h'f : ¬ (∀ᵐ ω ∂μ, f ω = 0)) (hindep : IndepFun f g μ) :
    IsProbabilityMeasure μ

Proof state:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
hindep : IndepFun f g μ
h'f : ∀ (c : ℝ≥0), 0 < c → μ {ω | c ≤ ‖f ω‖₊} ≤ 0
⊢ ∀ᵐ (ω : Ω) ∂μ, f ω = 0

Tactic:
have A (c : ℝ≥0) (hc : 0 < c) : ∀ᵐ ω ∂μ, ‖f ω‖₊ < c := by simpa [ae_iff] using h'f c hc

Result:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
hindep : IndepFun f g μ
h'f : ∀ (c : ℝ≥0), 0 < c → μ {ω | c ≤ ‖f ω‖₊} ≤ 0
A : ∀ (c : ℝ≥0), 0 < c → ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖₊ < c
⊢ ∀ᵐ (ω : Ω) ∂μ, f ω = 0

Proof state:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : IndepFun f g μ
⊢ ∃ c, 0 < c ∧ 0 < μ {ω | c ≤ ‖f ω‖₊}

Tactic:
contrapose! h'f

Result:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
hindep : IndepFun f g μ
h'f : ∀ (c : ℝ≥0), 0 < c → μ {ω | c ≤ ‖f ω‖₊} ≤ 0
⊢ ∀ᵐ (ω : Ω) ∂μ, f ω = 0

Proof state:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : IndepFun f g μ
⊢ IsProbabilityMeasure μ

Tactic:
obtain ⟨c, c_pos, hc⟩ : ∃ (c : ℝ≥0), 0 < c ∧ 0 < μ {ω | c ≤ ‖f ω‖₊} := by
  contrapose! h'f
  have A (c : ℝ≥0) (hc : 0 < c) : ∀ᵐ ω ∂μ, ‖f ω‖₊ < c := by simpa [ae_iff] using h'f c hc
  obtain ⟨u, -, u_pos, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n)
    ∧ Tendsto u atTop (𝓝 0) := exists_seq_strictAnti_tendsto (0 : ℝ≥0)
  filter_upwards [ae_all_iff.2 (fun n ↦ A (u n) (u_pos n))] with ω hω
  simpa using ge_of_tendsto' u_lim (fun i ↦ (hω i).le)

Result:
case intro.intro
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : IndepFun f g μ
c : ℝ≥0
c_pos : 0 < c
hc : 0 < μ {ω | c ≤ ‖f ω‖₊}
⊢ IsProbabilityMeasure μ

Proof state:
case intro.intro
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : IndepFun f g μ
c : ℝ≥0
c_pos : 0 < c
hc : 0 < μ {ω | c ≤ ‖f ω‖₊}
⊢ IsProbabilityMeasure μ

Tactic:
have h'c : μ {ω | c ≤ ‖f ω‖₊} < ∞ := hℒp.meas_ge_lt_top hp hp' c_pos.ne'

Result:
case intro.intro
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : IndepFun f g μ
c : ℝ≥0
c_pos : 0 < c
hc : 0 < μ {ω | c ≤ ‖f ω‖₊}
h'c : μ {ω | c ≤ ‖f ω‖₊} < ⊤
⊢ IsProbabilityMeasure μ

Proof state:
case intro.intro.intro
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
hindep : IndepFun f g μ
h'f : ∀ (c : ℝ≥0), 0 < c → μ {ω | c ≤ ‖f ω‖₊} ≤ 0
A : ∀ (c : ℝ≥0), 0 < c → ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖₊ < c
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
⊢ ∀ᵐ (ω : Ω) ∂μ, f ω = 0

Tactic:
filter_upwards [ae_all_iff.2 (fun n ↦ A (u n) (u_pos n))] with ω hω

Result:
case h
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
hindep : IndepFun f g μ
h'f : ∀ (c : ℝ≥0), 0 < c → μ {ω | c ≤ ‖f ω‖₊} ≤ 0
A : ∀ (c : ℝ≥0), 0 < c → ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖₊ < c
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
ω : Ω
hω : ∀ (i : ℕ), ‖f ω‖₊ < u i
⊢ f ω = 0

Proof state:
case h
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
hindep : IndepFun f g μ
h'f : ∀ (c : ℝ≥0), 0 < c → μ {ω | c ≤ ‖f ω‖₊} ≤ 0
A : ∀ (c : ℝ≥0), 0 < c → ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖₊ < c
u : ℕ → ℝ≥0
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
ω : Ω
hω : ∀ (i : ℕ), ‖f ω‖₊ < u i
⊢ f ω = 0

Tactic:
simpa using ge_of_tendsto' u_lim (fun i ↦ (hω i).le)

Result:
no goals

Proof state:
case intro.intro
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : IndepFun f g μ
c : ℝ≥0
c_pos : 0 < c
hc : 0 < μ {ω | c ≤ ‖f ω‖₊}
h'c : μ {ω | c ≤ ‖f ω‖₊} < ⊤
this : μ (f ⁻¹' {x | c ≤ ‖x‖₊} ∩ g ⁻¹' Set.univ) = μ (f ⁻¹' {x | c ≤ ‖x‖₊}) * μ (g ⁻¹' Set.univ)
⊢ IsProbabilityMeasure μ

Tactic:
simp only [Set.preimage_setOf_eq, Set.preimage_univ, Set.inter_univ] at this

Result:
case intro.intro
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
h'f : ¬∀ᵐ (ω : Ω) ∂μ, f ω = 0
hindep : IndepFun f g μ
c : ℝ≥0
c_pos : 0 < c
hc : 0 < μ {ω | c ≤ ‖f ω‖₊}
h'c : μ {ω | c ≤ ‖f ω‖₊} < ⊤
this : μ {a | c ≤ ‖f a‖₊} = μ {a | c ≤ ‖f a‖₊} * μ Set.univ
⊢ IsProbabilityMeasure μ

Proof state:
Ω : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : MeasurableSpace F
f : Ω → E
g : Ω → F
p : ℝ≥0∞
hp : p ≠ 0
hp' : p ≠ ⊤
hℒp : MemLp f p μ
hindep : IndepFun f g μ
h'f : ∀ (c : ℝ≥0), 0 < c → μ {ω | c ≤ ‖f ω‖₊} ≤ 0
c : ℝ≥0
hc : 0 < c
⊢ ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖₊ < c

Tactic:
simpa [ae_iff] using h'f c hc

Result:
no goals