awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
⊢ (∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) = lmarginal (X := A) μ {i} f x ^ (1 - k * p)
have h : (∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) =
  HPow.hPow (α := ℝ≥0∞) ((fun (x : (a : ι) → A a) ↦ ∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) x) (1 - k * p)
Tactic: rw [lmarginal_singleton]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
⊢ Eq (α := ℝ≥0∞) (∏ j ∈ s, (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p)
    (∏ j ∈ s, lmarginal (X := A) μ {i, j} f x ^ p)
have h : ∀ (j : ι) (hj : j ∈ s), (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p = lmarginal (X := A) μ {i, j} f x ^ p
Tactic: refine prod_congr rfl fun j hj => ?_
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
j : ι
hj : j ∈ s
⊢ i ∉ {j}
have simp : ¬i = j
Tactic: simp only [Finset.mem_singleton] at hj ⊢
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
j : ι
hj : j ∈ s
⊢ (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p = lmarginal (X := A) μ {i, j} f x ^ p
have hi' : i ∉ {j}
Tactic: have hi' : i ∉ ({j} : Finset ι) := by
                simp only [Finset.mem_singleton] at hj ⊢
                exact fun h ↦ hi (h ▸ hj)
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
j : ι
hj : j ∈ s
hi' : i ∉ {j}
⊢ (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p = lmarginal (X := A) μ {i, j} f x ^ p
have h : (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p =
  (∫⁻ (xᵢ : A i), lmarginal (X := A) μ {j} f (update (β := A) x i xᵢ) ∂μ i) ^ p
Tactic: rw [lmarginal_insert _ hf hi']
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
⊢ lmarginal (X := A) μ {i} f x ^ p *
      (lmarginal (X := A) μ {i} f x ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {i, j} f x ^ p) =
    lmarginal (X := A) μ {i} f x ^ (p + (1 - k * p)) * ∏ j ∈ s, lmarginal (X := A) μ {i, j} f x ^ p
have rw : lmarginal (X := A) μ {i} f x ^ p *
    (lmarginal (X := A) μ {i} f x ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {i, j} f x ^ p) =
  lmarginal (X := A) μ {i} f x ^ p * lmarginal (X := A) μ {i} f x ^ (1 - k * p) *
    ∏ j ∈ s, lmarginal (X := A) μ {i, j} f x ^ p
Tactic: rw [ENNReal.rpow_add_of_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
⊢ lmarginal (X := A) μ {i} f x ^ (p + (1 - k * p)) * ∏ j ∈ s, lmarginal (X := A) μ {i, j} f x ^ p ≤
    lmarginal (X := A) μ {i} f x ^ (1 - HSub.hSub (α := ℝ) (↑(#s) : ℝ) 1 * p) *
      ∏ j ∈ s, lmarginal (X := A) μ {j} (lmarginal (X := A) μ {i} f) x ^ p
have hxy : p + (1 - k * p) = 1 - HSub.hSub (α := ℝ) (↑(#s) : ℝ) 1 * p
Tactic: congr! 2 with j hj
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
hxy : p + (1 - k * p) = 1 - HSub.hSub (α := ℝ) (↑(#s) : ℝ) 1 * p
⊢ lmarginal (X := A) μ {i} f x ^ (p + (1 - k * p)) * ∏ j ∈ s, lmarginal (X := A) μ {i, j} f x ^ p ≤
    lmarginal (X := A) μ {i} f x ^ (1 - HSub.hSub (α := ℝ) (↑(#s) : ℝ) 1 * p) *
      ∏ j ∈ s, lmarginal (X := A) μ {j} (lmarginal (X := A) μ {i} f) x ^ p
have hxy₁ : ∀ (j : ι) (hj : j ∈ s),
  lmarginal (X := A) μ {i, j} f x ^ p = lmarginal (X := A) μ {j} (lmarginal (X := A) μ {i} f) x ^ p
Tactic: congr! 2 with j hj
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
j : ι
hj : j ∈ s
⊢ lmarginal (X := A) μ {i, j} f x ^ p = lmarginal (X := A) μ {j} (lmarginal (X := A) μ {i} f) x ^ p
have hxy : lmarginal (X := A) μ {i, j} f x = lmarginal (X := A) μ {j} (lmarginal (X := A) μ {i} f) x
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
j : ι
hj : j ∈ s
⊢ lmarginal (X := A) μ {i, j} f x = lmarginal (X := A) μ {j} (lmarginal (X := A) μ {i} f) x
have hxy : lmarginal (X := A) μ {i, j} f x = lmarginal (X := A) μ ({j} ∪ {i}) f x
Tactic: rw [← lmarginal_union μ f hf]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
j : ι
hj : j ∈ s
hxy : lmarginal (X := A) μ {i, j} f x = lmarginal (X := A) μ ({j} ∪ {i}) f x
⊢ lmarginal (X := A) μ {i, j} f x = lmarginal (X := A) μ {j} (lmarginal (X := A) μ {i} f) x
have hxy₁ : Disjoint (α := Finset ι) {j} {i}
Tactic: rw [← lmarginal_union μ f hf]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
j : ι
hj : j ∈ s
⊢ lmarginal (X := A) μ {i, j} f x = lmarginal (X := A) μ ({j} ∪ {i}) f x
have hxy : Eq (α := Finset ι) {i, j} ({j} ∪ {i})
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
j : ι
hj : j ∈ s
⊢ Eq (α := Finset ι) {i, j} ({j} ∪ {i})
have hxy : Eq (α := Finset ι) {i, j} ({i} ∪ {j})
Tactic: rw [Finset.union_comm]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
s : Finset ι
hp : (↑(#s) : ℝ) * p ≤ 1
i : ι
hi : i ∉ s
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
x : (i : ι) → A i
X : (v : A i) → (a : ι) → A a := update (β := A) x i
hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
k : ℝ := (↑(#s) : ℝ)
hk' : 0 ≤ 1 - k * p
j : ι
hj : j ∈ s
⊢ Disjoint (α := Finset ι) {j} {i}
have hxy : j ≠ i
Tactic: rw [Finset.disjoint_singleton]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ Antitone (β := ((i : ι) → A i) → ℝ≥0∞) fun (s : Finset ι) ↦ T (A := A) μ p (lmarginal (X := A) μ sᶜ f) s
have rw : ∀ (s : Finset ι) ⦃a : ι⦄,
  a ∉ s →
    T (A := A) μ p (lmarginal (X := A) μ (insert a s)ᶜ f) (insert a s) ≤ T (A := A) μ p (lmarginal (X := A) μ sᶜ f) s
Tactic: rw [Finset.antitone_iff_forall_insert_le]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ T (A := A) μ p (lmarginal (X := A) μ (insert i s)ᶜ f) (insert i s) ≤ T (A := A) μ p (lmarginal (X := A) μ sᶜ f) s
have h : lmarginal (X := A) μ sᶜ f = lmarginal (X := A) μ {i} (lmarginal (X := A) μ (insert i s)ᶜ f)
Tactic: convert! T_insert_le_T_lmarginal_singleton μ hp₀ s ?_ i hi (hf.lmarginal μ) using 2
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
h : lmarginal (X := A) μ sᶜ f = lmarginal (X := A) μ {i} (lmarginal (X := A) μ (insert i s)ᶜ f)
⊢ T (A := A) μ p (lmarginal (X := A) μ (insert i s)ᶜ f) (insert i s) ≤ T (A := A) μ p (lmarginal (X := A) μ sᶜ f) s
have convert_1 : (↑(#s) : ℝ) * p ≤ 1
Tactic: convert! T_insert_le_T_lmarginal_singleton μ hp₀ s ?_ i hi (hf.lmarginal μ) using 2
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ lmarginal (X := A) μ sᶜ f = lmarginal (X := A) μ {i} (lmarginal (X := A) μ (insert i s)ᶜ f)
have h : lmarginal (X := A) μ sᶜ f = lmarginal (X := A) μ ({i} ∪ (insert i s)ᶜ) f
Tactic: rw [← lmarginal_union μ f hf]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
h : lmarginal (X := A) μ sᶜ f = lmarginal (X := A) μ ({i} ∪ (insert i s)ᶜ) f
⊢ lmarginal (X := A) μ sᶜ f = lmarginal (X := A) μ {i} (lmarginal (X := A) μ (insert i s)ᶜ f)
have h₁ : Disjoint {i} (insert i s)ᶜ
Tactic: rw [← lmarginal_union μ f hf]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ lmarginal (X := A) μ sᶜ f = lmarginal (X := A) μ ({i} ∪ (insert i s)ᶜ) f
have h : lmarginal (X := A) μ (insert i (insert i s)ᶜ) f = lmarginal (X := A) μ ({i} ∪ (insert i s)ᶜ) f
Tactic: rw [← insert_compl_insert hi]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ Disjoint {i} (insert i s)ᶜ
have h : i ∈ insert i s
Tactic: rw [Finset.disjoint_singleton_left, notMem_compl]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ (↑(#s) : ℝ) * p ≤ 1
have convert_1 : (↑(#s) : ℝ) * p ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p
Tactic: refine le_trans ?_ hp
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ (↑(#s) : ℝ) * p ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p
have convert_1 : (↑(#s) : ℝ) ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
this : HAdd.hAdd (α := ℝ) (↑(#s) : ℝ) 1 ≤ (↑#ι : ℝ)
⊢ (↑(#s) : ℝ) ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
have linarith : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 < (↑(#s) : ℝ) →
  HAdd.hAdd (α := ℝ) (↑(#s) : ℝ) 1 - (↑#ι : ℝ) + (HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 - (↑(#s) : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ (↑(#s) : ℝ) ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
have convert_1 : HAdd.hAdd (α := ℝ) (↑(#s) : ℝ) 1 ≤ (↑#ι : ℝ)
Tactic: suffices (s.card : ℝ) + 1 ≤ #ι by linarith
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ HAdd.hAdd (α := ℝ) (↑(#s) : ℝ) 1 ≤ (↑#ι : ℝ)
have convert_1 : HAdd.hAdd (α := ℝ) (↑(#s) : ℝ) 1 ≤ (↑(#s + #sᶜ) : ℝ)
Tactic: rw [← card_add_card_compl s]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ HAdd.hAdd (α := ℝ) (↑(#s) : ℝ) 1 ≤ (↑(#s + #sᶜ) : ℝ)
have convert_1 : #s + 1 ≤ #s + #sᶜ
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ #s + 1 ≤ #s + #sᶜ
have convert_1 : 1 ≤ #sᶜ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
⊢ 1 ≤ #sᶜ
have hi' : sᶜ.Nonempty
Tactic: have hi' : sᶜ.Nonempty := ⟨i, by rwa [Finset.mem_compl]⟩
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
p : ℝ
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
s : Finset ι
i : ι
hi : i ∉ s
hi' : sᶜ.Nonempty
⊢ 1 ≤ #sᶜ
have convert_1 : ∀ (hi' : 0 < #sᶜ), 1 ≤ #sᶜ
Tactic: rwa [← card_pos] at hi'
Cleared hypotheses: hi'
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p) *
        ∏ i : ι, (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ p ∂Measure.pi (α := A) μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ (1 + p)
have inl : IsEmpty ((i : ι) → A i) →
  ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p) *
        ∏ i : ι, (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ p ∂Measure.pi (α := A) μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ (1 + p)
Tactic: cases isEmpty_or_nonempty (∀ i, A i)
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
A : ι → Type u_2
inst : (i : ι) → MeasurableSpace (A i)
μ : (i : ι) → Measure (A i)
inst_1 : DecidableEq ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp₀ : 0 ≤ p
hp : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p ≤ 1
f : ((i : ι) → A i) → ℝ≥0∞
hf : Measurable f
inl :
  IsEmpty ((i : ι) → A i) →
    ∫⁻ (x : (i : ι) → A i),
        f x ^ (1 - HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p) *
          ∏ i : ι, (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ p ∂Measure.pi (α := A) μ ≤
      (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ (1 + p)
⊢ ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p) *
        ∏ i : ι, (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ p ∂Measure.pi (α := A) μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ (1 + p)
have inr : Nonempty ((i : ι) → A i) →
  ∫⁻ (x : (i : ι) → A i),
      f x ^ (1 - HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p) *
        ∏ i : ι, (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ p ∂Measure.pi (α := A) μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ (1 + p)
Tactic: cases isEmpty_or_nonempty (∀ i, A i)