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
⊢ Measurable (β := ℝ≥0∞) fun (x : (i : ι) → A i) ↦
    HMul.hMul (β := (x : (i : ι) → A i) → ℝ≥0∞) (f ^ (1 - (↑(#s) : ℝ) * p))
      (∏ j ∈ insert i s, lmarginal (X := A) μ {j} f ^ p) x
have simp : Measurable (β := ℝ≥0∞) fun (x : (i : ι) → A i) ↦
  f x ^ (1 - (↑(#s) : ℝ) * p) * ∏ x_1 ∈ insert i s, lmarginal (X := A) μ {x_1} f x ^ p
Tactic: simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]
-- 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
⊢ Measurable (β := ℝ≥0∞) fun (x : (i : ι) → A i) ↦
    f x ^ (1 - (↑(#s) : ℝ) * p) * ∏ x_1 ∈ insert i s, lmarginal (X := A) μ {x_1} f x ^ p
have refine : ∀ i_1 ∈ insert i s, Measurable (β := ℝ≥0∞) fun (x : (i : ι) → A i) ↦ lmarginal (X := A) μ {i_1} f x ^ p
Tactic: refine (hf.pow_const _).mul <| Finset.measurable_fun_prod _ ?_
-- 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
⊢ T (A := A) μ p f (insert i s) ≤ T (A := A) μ p (lmarginal (X := A) μ {i} f) s
have calc : ∀ (x : (i : ι) → A i),
  ∫⁻ (t : A i),
      f (update (β := A) x i t) ^ (1 - (↑(#s) : ℝ) * p) *
        ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (update (β := A) x i t) ^ p ∂μ i ≤
    HMul.hMul (β := (x : (i : ι) → A i) → ℝ≥0∞)
      (lmarginal (X := A) μ {i} f ^ (1 - HSub.hSub (α := ℝ) (↑(#s) : ℝ) 1 * p))
      (∏ i_1 ∈ s, lmarginal (X := A) μ {i_1} (lmarginal (X := A) μ {i} f) ^ p) x
Tactic: calc T μ p f (insert i s)
      = ∫⋯∫⁻_insert i s,
            f ^ (1 - (s.card : ℝ) * p) * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) ^ p ∂μ := by
          -- unfold `T` and reformulate the exponents
          simp_rw [T, card_insert_of_notMem hi]
          congr!
          push_cast
          ring
    _ = ∫⋯∫⁻_s, (fun x ↦ ∫⁻ (t : A i),
            (f (update x i t) ^ (1 - (s.card : ℝ) * p)
            * ∏ j ∈ insert i s, (∫⋯∫⁻_{j}, f ∂μ) (update x i t) ^ p) ∂(μ i)) ∂μ := by
          -- pull out the integral over `xᵢ`
          rw [lmarginal_insert' _ _ hi]
          · simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]
          · change Measurable (fun x ↦ _)
            simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]
            refine (hf.pow_const _).mul <| Finset.measurable_fun_prod _ ?_
            exact fun _ _ ↦ hf.lmarginal μ |>.pow_const _
    _ ≤ T μ p (∫⋯∫⁻_{i}, f ∂μ) s := lmarginal_mono (s := s) (fun x ↦ ?_)
-- 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
⊢ ∫⁻ (t : A i),
      f (update (β := A) x i t) ^ (1 - (↑(#s) : ℝ) * p) *
        ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (update (β := A) x i t) ^ p ∂μ i ≤
    HMul.hMul (β := (x : (i : ι) → A i) → ℝ≥0∞)
      (lmarginal (X := A) μ {i} f ^ (1 - HSub.hSub (α := ℝ) (↑(#s) : ℝ) 1 * p))
      (∏ i_1 ∈ s, lmarginal (X := A) μ {i_1} (lmarginal (X := A) μ {i} f) ^ p) x
have simp : ∫⁻ (t : A i),
    f (update (β := A) x i t) ^ (1 - (↑(#s) : ℝ) * p) *
      ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (update (β := A) x i t) ^ p ∂μ i ≤
  lmarginal (X := A) μ {i} f x ^ (1 - HSub.hSub (α := ℝ) (↑(#s) : ℝ) 1 * p) *
    ∏ x_1 ∈ s, lmarginal (X := A) μ {x_1} (lmarginal (X := A) μ {i} f) x ^ p
Tactic: simp only [Pi.mul_apply, Pi.pow_apply, Finset.prod_apply]
-- 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
⊢ ∫⁻ (t : A i), f (X t) ^ (1 - (↑(#s) : ℝ) * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i ≤
    lmarginal (X := A) μ {i} f x ^ (1 - HSub.hSub (α := ℝ) (↑(#s) : ℝ) 1 * p) *
      ∏ x_1 ∈ s, lmarginal (X := A) μ {x_1} (lmarginal (X := A) μ {i} f) x ^ p
have hF₁ : ∀ {j : ι}, Measurable (β := ℝ≥0∞) fun (t : A i) ↦ lmarginal (X := A) μ {j} f (X t)
Tactic: have hF₁ : ∀ {j : ι}, Measurable fun t ↦ (∫⋯∫⁻_{j}, f ∂μ) (X t) :=
    fun {_} ↦ hf.lmarginal μ |>.comp <| measurable_update _
-- 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)
⊢ ∫⁻ (t : A i), f (X t) ^ (1 - (↑(#s) : ℝ) * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i ≤
    lmarginal (X := A) μ {i} f x ^ (1 - HSub.hSub (α := ℝ) (↑(#s) : ℝ) 1 * p) *
      ∏ x_1 ∈ s, lmarginal (X := A) μ {x_1} (lmarginal (X := A) μ {i} f) x ^ p
have hF₀ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t)
Tactic: have hF₀ : Measurable fun t ↦ f (X t) := hf.comp <| measurable_update _
-- 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) : ℝ)
⊢ 0 ≤ 1 - k * p
have linarith : 1 - k * p < 0 → 1 - k * p - 0 + ((↑(#s) : ℝ) * p - 1) = 0
Tactic: linarith only [hp]
-- 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) : ℝ)
⊢ ∫⁻ (t : A i), f (X t) ^ (1 - (↑(#s) : ℝ) * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i ≤
    lmarginal (X := A) μ {i} f x ^ (1 - HSub.hSub (α := ℝ) (↑(#s) : ℝ) 1 * p) *
      ∏ x_1 ∈ s, lmarginal (X := A) μ {x_1} (lmarginal (X := A) μ {i} f) x ^ p
have hk' : 0 ≤ 1 - k * p
Tactic: have hk' : 0 ≤ 1 - k * p := by linarith only [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 : ∀ (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) ^ (1 - k * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i =
    ∫⁻ (t : A i),
      lmarginal (X := A) μ {i} f (X t) ^ p *
        (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p) ∂μ i
have clear_value : ∀ (X : (v : A i) → (a : ι) → A a)
  (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)),
  let k : ℝ := (↑(#s) : ℝ);
  ∀ (hk' : 0 ≤ 1 - k * p),
    ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i =
      ∫⁻ (t : A i),
        lmarginal (X := A) μ {i} f (X t) ^ p *
          (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p) ∂μ i
Tactic: clear_value X
Cleared hypotheses: X, hF₁, hF₀, k, hk'
-- 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
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) ^ (1 - k * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i =
    ∫⁻ (t : A i),
      lmarginal (X := A) μ {i} f (X t) ^ p *
        (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p) ∂μ i
have h : ∀ (t : A i),
  f (X t) ^ (1 - k * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (X t) ^ p =
    lmarginal (X := A) μ {i} f (X t) ^ p * (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p)
Tactic: congr! 2 with t
-- 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
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) ^ (1 - k * p) * ∏ j ∈ insert i s, lmarginal (X := A) μ {j} f (X t) ^ p =
    lmarginal (X := A) μ {i} f (X t) ^ p * (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p)
have h : f (X t) ^ (1 - k * p) * (lmarginal (X := A) μ {i} f (X t) ^ p * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p) =
  lmarginal (X := A) μ {i} f (X t) ^ p * (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p)
Tactic: simp_rw [prod_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 : ∀ (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
⊢ lmarginal (X := A) μ {i} f (X t) = lmarginal (X := A) μ {i} f x
have hi₁ : Membership.mem (γ := Finset ι) {i} i
Tactic: rw [lmarginal_update_of_mem]
-- 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
⊢ ∫⁻ (t : A i),
      lmarginal (X := A) μ {i} f (X t) ^ p *
        (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p) ∂μ i =
    lmarginal (X := A) μ {i} f x ^ p *
      ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i
have this : ∀ (t : A i), lmarginal (X := A) μ {i} f (X t) = lmarginal (X := A) μ {i} f x
Tactic: have : ∀ t, (∫⋯∫⁻_{i}, f ∂μ) (X t) = (∫⋯∫⁻_{i}, f ∂μ) x := by
                intro t
                rw [lmarginal_update_of_mem]
                exact Iff.mpr Finset.mem_singleton rfl
-- 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
this : ∀ (t : A i), lmarginal (X := A) μ {i} f (X t) = lmarginal (X := A) μ {i} f x
⊢ ∫⁻ (t : A i),
      lmarginal (X := A) μ {i} f (X t) ^ p *
        (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p) ∂μ i =
    lmarginal (X := A) μ {i} f x ^ p *
      ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i
have simp_rw : ∫⁻ (t : A i),
    lmarginal (X := A) μ {i} f x ^ p * (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p) ∂μ i =
  lmarginal (X := A) μ {i} f x ^ p *
    ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i
Tactic: simp_rw [this]
-- 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
this : ∀ (t : A i), lmarginal (X := A) μ {i} f (X t) = lmarginal (X := A) μ {i} f x
⊢ ∫⁻ (t : A i),
      lmarginal (X := A) μ {i} f x ^ p * (f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p) ∂μ i =
    lmarginal (X := A) μ {i} f x ^ p *
      ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i
have hf₁ : Measurable (β := ℝ≥0∞) fun (t : A i) ↦ f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p
Tactic: rw [lintegral_const_mul]
-- 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 *
      ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i ≤
    lmarginal (X := A) μ {i} f x ^ p *
      ((∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) * ∏ j ∈ s, (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p)
have bc : ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i ≤
  (∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) * ∏ j ∈ s, (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p
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 : ∀ (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) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i ≤
    (∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) * ∏ j ∈ s, (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p
have bc : AEMeasurable (β := ℝ≥0∞) (fun (a : A i) ↦ f (X a)) (μ i)
Tactic: apply ENNReal.lintegral_mul_prod_norm_pow_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 : ∀ (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
bc : AEMeasurable (β := ℝ≥0∞) (fun (a : A i) ↦ f (X a)) (μ i)
⊢ ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i ≤
    (∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) * ∏ j ∈ s, (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p
have bc₁ : ∀ i_1 ∈ s, AEMeasurable (β := ℝ≥0∞) (fun (a : A i) ↦ lmarginal (X := A) μ {i_1} f (X a)) (μ i)
Tactic: apply ENNReal.lintegral_mul_prod_norm_pow_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 : ∀ (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
bc : AEMeasurable (β := ℝ≥0∞) (fun (a : A i) ↦ f (X a)) (μ i)
bc₁ : ∀ i_1 ∈ s, AEMeasurable (β := ℝ≥0∞) (fun (a : A i) ↦ lmarginal (X := A) μ {i_1} f (X a)) (μ i)
⊢ ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i ≤
    (∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) * ∏ j ∈ s, (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p
have bc₂ : 1 - k * p + ∑ i ∈ s, p = 1
Tactic: apply ENNReal.lintegral_mul_prod_norm_pow_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 : ∀ (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
bc : AEMeasurable (β := ℝ≥0∞) (fun (a : A i) ↦ f (X a)) (μ i)
bc₁ : ∀ i_1 ∈ s, AEMeasurable (β := ℝ≥0∞) (fun (a : A i) ↦ lmarginal (X := A) μ {i_1} f (X a)) (μ i)
bc₂ : 1 - k * p + ∑ i ∈ s, p = 1
bc₃ : 0 ≤ 1 - k * p
⊢ ∫⁻ (t : A i), f (X t) ^ (1 - k * p) * ∏ j ∈ s, lmarginal (X := A) μ {j} f (X t) ^ p ∂μ i ≤
    (∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) * ∏ j ∈ s, (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ p
have bc₄ : ∀ i ∈ s, 0 ≤ p
Tactic: apply ENNReal.lintegral_mul_prod_norm_pow_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 : ∀ (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
⊢ 1 - k * p + ∑ i ∈ s, p = 1
have bc : 1 - k * p + (↑(#s) : ℝ) * p = 1
Tactic: simp only [sum_const, nsmul_eq_mul]
-- 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 *
      ((∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) *
        ∏ j ∈ s, (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ 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)
have h : (∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) = lmarginal (X := A) μ {i} f x ^ (1 - k * p)
Tactic: congr! 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 : ∀ (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
h : (∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) = lmarginal (X := A) μ {i} f x ^ (1 - k * p)
⊢ lmarginal (X := A) μ {i} f x ^ p *
      ((∫⁻ (t : A i), f (X t) ∂μ i) ^ (1 - k * p) *
        ∏ j ∈ s, (∫⁻ (t : A i), lmarginal (X := A) μ {j} f (X t) ∂μ i) ^ 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)
have h₁ : 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)
Tactic: congr! 2