-- Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean
theorem lintegral_mul_prod_lintegral_pow_le
    [Fintype ι] [∀ i, SigmaFinite (μ i)] {p : ℝ} (hp₀ : 0 ≤ p)
    (hp : (#ι - 1 : ℝ) * p ≤ 1) {f : (∀ i : ι, A i) → ℝ≥0∞} (hf : Measurable f) :
    ∫⁻ x, f x ^ (1 - (#ι - 1 : ℝ) * p) * ∏ i, (∫⁻ xᵢ, f (update x i xᵢ) ∂μ i) ^ p ∂.pi μ
    ≤ (∫⁻ x, f x ∂.pi μ) ^ (1 + p)

Proof state:
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - (↑#ι - 1) * p) * ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)

Tactic:
cases isEmpty_or_nonempty (∀ i, A i)

Result:
case inl
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h✝ : IsEmpty ((i : ι) → A i)
⊢ ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - (↑#ι - 1) * p) * ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)

case inr
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h✝ : Nonempty ((i : ι) → A i)
⊢ ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - (↑#ι - 1) * p) * ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)

Proof state:
case inr
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h✝ : Nonempty ((i : ι) → A i)
inhabited_h : Inhabited ((i : ι) → A i)
H : ∅ ≤ Finset.univ
⊢ ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - (↑#ι - 1) * p) * ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)

Tactic:
simpa [lmarginal_univ] using GridLines.T_lmarginal_antitone μ hp₀ hp hf H default

Result:
no goals

Proof state:
case inl
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h✝ : IsEmpty ((i : ι) → A i)
⊢ ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - (↑#ι - 1) * p) * ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)

Tactic:
simp_rw [lintegral_of_isEmpty]

Result:
case inl
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h✝ : IsEmpty ((i : ι) → A i)
⊢ 0 ≤ 0 ^ (1 + p)

Proof state:
case inr
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h✝ : Nonempty ((i : ι) → A i)
inhabited_h : Inhabited ((i : ι) → A i)
⊢ ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - (↑#ι - 1) * p) * ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)

Tactic:
have H : (∅ : Finset ι) ≤ Finset.univ := Finset.empty_subset _

Result:
case inr
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h✝ : Nonempty ((i : ι) → A i)
inhabited_h : Inhabited ((i : ι) → A i)
H : ∅ ≤ Finset.univ
⊢ ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - (↑#ι - 1) * p) * ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)

Proof state:
case inl
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h✝ : IsEmpty ((i : ι) → A i)
⊢ 0 ≤ 0 ^ (1 + p)

Tactic:
refine zero_le _

Result:
no goals

Proof state:
case inr
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h✝ : Nonempty ((i : ι) → A i)
⊢ ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - (↑#ι - 1) * p) * ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)

Tactic:
inhabit ∀ i, A i

Result:
case inr
ι : Type u_1
A : ι → Type u_2
inst✝³ : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : (↑#ι - 1) * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
h✝ : Nonempty ((i : ι) → A i)
inhabited_h : Inhabited ((i : ι) → A i)
⊢ ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - (↑#ι - 1) * p) * ∏ i : ι, (∫⁻ (xᵢ : A i), f (update x i xᵢ) ∂μ i) ^ p ∂Measure.pi μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi μ) ^ (1 + p)