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 ι
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
h : 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)
have inr : ∀ (inhabited_h : Inhabited ((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: inhabit ∀ i, A i
-- 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 ι
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
h : Nonempty ((i : ι) → A i)
inhabited_h : Inhabited ((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)
have H : LE.le.{u_1} (α := Finset ι) ∅ Finset.univ
Tactic: have H : (∅ : Finset ι) ≤ Finset.univ := Finset.empty_subset _
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
⊢ ∫⁻ (x : (i : ι) → A i),
      ∏ i : ι,
        (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ∂Measure.pi (α := A) μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ p
have this : Nontrivial ι
Tactic: have : Nontrivial ι :=
    Fintype.one_lt_card_iff_nontrivial.mp (by exact_mod_cast hp.lt)
-- 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 : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
⊢ LT.lt (α := ℝ) 1 (↑#ι : ℝ)
have norm_cast : 1 < #ι
Tactic: norm_cast
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
⊢ ∫⁻ (x : (i : ι) → A i),
      ∏ i : ι,
        (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ∂Measure.pi (α := A) μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ p
have h0 : LT.lt (α := ℝ) 1 (↑#ι : ℝ)
Tactic: have h0 : (1 : ℝ) < #ι := by norm_cast; exact Fintype.one_lt_card
-- 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 : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
h0 : LT.lt (α := ℝ) 1 (↑#ι : ℝ)
⊢ 0 < HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
have linarith : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 ≤ 0 → HSub.hSub (α := ℝ) 1 (↑#ι : ℝ) + (HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 - 0) = 0
Tactic: linarith
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
h0 : LT.lt (α := ℝ) 1 (↑#ι : ℝ)
⊢ ∫⁻ (x : (i : ι) → A i),
      ∏ i : ι,
        (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ∂Measure.pi (α := A) μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ p
have h1 : 0 < HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
Tactic: have h1 : (0 : ℝ) < #ι - 1 := by linarith
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
h0 : LT.lt (α := ℝ) 1 (↑#ι : ℝ)
h1 : 0 < HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
⊢ ∫⁻ (x : (i : ι) → A i),
      ∏ i : ι,
        (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ∂Measure.pi (α := A) μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ p
have h2 : 0 ≤ 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
Tactic: have h2 : 0 ≤ ((1 : ℝ) / (#ι - 1 : ℝ)) := by positivity
-- 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 : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
h0 : LT.lt (α := ℝ) 1 (↑#ι : ℝ)
h1 : 0 < HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
h2 : 0 ≤ 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
⊢ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ≤ 1
have field_simp : LE.le (α := ℝ) 1 1
Tactic: field_simp
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
h0 : LT.lt (α := ℝ) 1 (↑#ι : ℝ)
h1 : 0 < HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
h2 : 0 ≤ 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
⊢ ∫⁻ (x : (i : ι) → A i),
      ∏ i : ι,
        (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ∂Measure.pi (α := A) μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ p
have h3 : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ≤ 1
Tactic: have h3 : (#ι - 1 : ℝ) * ((1 : ℝ) / (#ι - 1 : ℝ)) ≤ 1 := by field_simp; 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
h0 : LT.lt (α := ℝ) 1 (↑#ι : ℝ)
h1 : 0 < HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
h2 : 0 ≤ 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
h3 : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ≤ 1
⊢ p = 1 + 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
have simp : p * HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 = (↑#ι : ℝ)
Tactic: simp [field]
-- 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 : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
h0 : LT.lt (α := ℝ) 1 (↑#ι : ℝ)
h1 : 0 < HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
h2 : 0 ≤ 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
h3 : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ≤ 1
⊢ p * HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 = (↑#ι : ℝ)
have rw : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p = (↑#ι : ℝ)
Tactic: rw [mul_comm, hp.sub_one_mul_conj]
-- 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 : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
h0 : LT.lt (α := ℝ) 1 (↑#ι : ℝ)
h1 : 0 < HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
h2 : 0 ≤ 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
h3 : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ≤ 1
rw : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * p = (↑#ι : ℝ)
⊢ p * HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 = (↑#ι : ℝ)
have rw₁ : Eq (α := ℝ) (↑#ι : ℝ) (↑#ι : ℝ)
Tactic: rw [mul_comm, hp.sub_one_mul_conj]
-- 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
h0 : LT.lt (α := ℝ) 1 (↑#ι : ℝ)
h1 : 0 < HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
h2 : 0 ≤ 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
h3 : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ≤ 1
⊢ ∫⁻ (x : (i : ι) → A i),
      ∏ i : ι,
        (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ∂Measure.pi (α := A) μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ p
have h4 : p = 1 + 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
Tactic: have h4 : p = 1 + 1 / (↑#ι - 1) := by simp [field]; rw [mul_comm, hp.sub_one_mul_conj]
-- 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 : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
h0 : LT.lt (α := ℝ) 1 (↑#ι : ℝ)
h1 : 0 < HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
h2 : 0 ≤ 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
h3 : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ≤ 1
h4 : p = 1 + 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
⊢ ∫⁻ (x : (i : ι) → A i),
      ∏ i : ι,
        (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ∂Measure.pi (α := A) μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ p
have rw : ∫⁻ (x : (i : ι) → A i),
    ∏ i : ι,
      (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ∂Measure.pi (α := A) μ ≤
  (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ (1 + 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)
Tactic: rw [h4]
-- 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 : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
h0 : LT.lt (α := ℝ) 1 (↑#ι : ℝ)
h1 : 0 < HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
h2 : 0 ≤ 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
h3 : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ≤ 1
h4 : p = 1 + 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
⊢ ∫⁻ (x : (i : ι) → A i),
      ∏ i : ι,
        (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ∂Measure.pi (α := A) μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ (1 + 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)
have h : Eq (α := ((i : ι) → A i) → ℝ≥0∞)
  (fun (x : (i : ι) → A i) ↦
    ∏ i : ι, (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1))
  fun (x : (i : ι) → A i) ↦
  f x ^ (1 - HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) *
    ∏ i : ι, (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)
Tactic: convert! lintegral_mul_prod_lintegral_pow_le μ h2 h3 hf 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 ι
inst_2 : Fintype ι
inst_3 : ∀ (i : ι), SigmaFinite (μ i)
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
f : ((a : ι) → A a) → ℝ≥0∞
hf : Measurable f
this : Nontrivial ι
h0 : LT.lt (α := ℝ) 1 (↑#ι : ℝ)
h1 : 0 < HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
h2 : 0 ≤ 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
h3 : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ≤ 1
h4 : p = 1 + 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
⊢ Eq (α := ((i : ι) → A i) → ℝ≥0∞)
    (fun (x : (i : ι) → A i) ↦
      ∏ i : ι, (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1))
    fun (x : (i : ι) → A i) ↦
    f x ^ (1 - HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) *
      ∏ i : ι, (∫⁻ (xᵢ : A i), f (update (β := A) x i xᵢ) ∂μ i) ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)
have h : Eq (α := ((i : ι) → A i) → ℝ≥0∞)
  (fun (x : (i : ι) → A i) ↦
    ∏ x_1 : ι, (∫⁻ (xᵢ : A x_1), f (update (β := A) x x_1 xᵢ) ∂μ x_1) ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1))
  fun (x : (i : ι) → A i) ↦
  f x ^ HSub.hSub (α := ℝ) 1 1 *
    ∏ x_1 : ι, (∫⁻ (xᵢ : A x_1), f (update (β := A) x x_1 xᵢ) ∂μ x_1) ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
⊢ 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
have hι : LE.le (α := ℝ) 2 (↑#ι : ℝ)
Tactic: have hι : (2 : ℝ) ≤ #ι := by exact_mod_cast hp.lt
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
hι : LE.le (α := ℝ) 2 (↑#ι : ℝ)
⊢ 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
have linarith : HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 < 1 → HSub.hSub (α := ℝ) 2 (↑#ι : ℝ) + (HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (hypothesis)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
⊢ ∫⁻ (x : ι → ℝ), ‖u x‖ₑ ^ p ≤
    (∫⁻ (x : ι → ℝ), enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F) (fderiv ℝ u x)) ^ p
have this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
Tactic: have : (1 : ℝ) ≤ ↑#ι - 1 := by
    have hι : (2 : ℝ) ≤ #ι := by exact_mod_cast hp.lt
    linarith
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
⊢ ∫⁻ (x : ι → ℝ), ‖u x‖ₑ ^ p =
    ∫⁻ (x : ι → ℝ), HPow.hPow (β := ℝ) (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) (↑#ι : ℝ)
have h : ∀ (x : ι → ℝ), ‖u x‖ₑ ^ p = HPow.hPow (β := ℝ) (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) (↑#ι : ℝ)
Tactic: congr! 2 with x
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
⊢ ‖u x‖ₑ ^ p = HPow.hPow (β := ℝ) (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) (↑#ι : ℝ)
have h : ‖u x‖ₑ ^ ((↑#ι : ℝ) / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) = ‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * (↑#ι : ℝ))
Tactic: rw [← ENNReal.rpow_mul, hp.conjugate_eq]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
⊢ ∫⁻ (x : ι → ℝ), HPow.hPow (β := ℝ) (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) (↑#ι : ℝ) =
    ∫⁻ (x : ι → ℝ), ∏ _i : ι, ‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)
have h : ∀ (x : ι → ℝ),
  HPow.hPow (β := ℝ) (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) (↑#ι : ℝ) =
    ∏ _i : ι, ‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)
Tactic: congr! 2 with x
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
⊢ HPow.hPow (β := ℝ) (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) (↑#ι : ℝ) =
    ∏ _i : ι, ‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)
have h : HPow.hPow (β := ℝ) (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) (↑#ι : ℝ) =
  (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) ^ card.{u_1} (α := ι) Finset.univ
Tactic: simp_rw [prod_const]
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
x : ι → ℝ
⊢ HPow.hPow (β := ℝ) (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) (↑#ι : ℝ) =
    (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) ^ card.{u_1} (α := ι) Finset.univ
have h : HPow.hPow (β := ℝ) ‖u x‖ₑ (↑(Rat.divInt 1 (Int.subNatNat (#ι) 1)) : ℝ) ^ #ι =
  HPow.hPow (β := ℝ) ‖u x‖ₑ (↑(Rat.divInt 1 (Int.subNatNat (#ι) 1)) : ℝ) ^ card.{u_1} (α := ι) Finset.univ
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
⊢ ∫⁻ (x : (a : ι) → ℝ),
      ∏ i : ι,
        (∫⁻ (xᵢ : ℝ),
            enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
              (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i xᵢ))) ^
          (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ≤
    (∫⁻ (x : ι → ℝ), enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F) (fderiv ℝ u x)) ^ p
have apply : Measurable (β := ℝ≥0∞) fun (x : (i : ι) → ℝ) ↦
  enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F) (fderiv ℝ u x)
Tactic: apply lintegral_prod_lintegral_pow_le _ hp
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
⊢ Measurable (β := ℝ≥0∞) fun (x : (i : ι) → ℝ) ↦
    enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F) (fderiv ℝ u x)
have funProp : FinStronglyMeasurable (β := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
  (fun (x : ι → ℝ) ↦ fderiv ℝ u x) ?μ
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
funProp :
  FinStronglyMeasurable (β := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
    (fun (x : ι → ℝ) ↦ fderiv ℝ u x) ?μ
⊢ Measurable (β := ℝ≥0∞) fun (x : (i : ι) → ℝ) ↦
    enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F) (fderiv ℝ u x)
have funProp₁ : LE.le.{u_1} (α := MeasurableSpace ((i : ι) → ℝ)) (MeasurableSpace.pi (X := fun (i : ι) ↦ ℝ))
  (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
funProp :
  FinStronglyMeasurable (β := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
    (fun (x : ι → ℝ) ↦ fderiv ℝ u x) ?μ
funProp₁ :
  LE.le.{u_1} (α := MeasurableSpace ((i : ι) → ℝ)) (MeasurableSpace.pi (X := fun (i : ι) ↦ ℝ))
    (MeasurableSpace.pi (X := fun (a : ι) ↦ ℝ))
⊢ Measurable (β := ℝ≥0∞) fun (x : (i : ι) → ℝ) ↦
    enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F) (fderiv ℝ u x)
have funProp₂ : MeasurableEmbedding (β := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F) fun (x : (i : ι) → ℝ) ↦
  fderiv ℝ u x
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Analysis.FunctionalSpaces.SobolevInequality (goal)
Goal:
ι : Type u_1
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : Fintype ι
p : ℝ
hp : Real.HolderConjugate (↑#ι : ℝ) p
u : (ι → ℝ) → F
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
this : 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1
⊢ ∫⁻ (x : ι → ℝ), ‖u x‖ₑ ^ p ≤
    (∫⁻ (x : ι → ℝ), enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F) (fderiv ℝ u x)) ^ p
have calc : ∫⁻ (x : ι → ℝ), ∏ _i : ι, ‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ≤
  ∫⁻ (x : (a : ι) → ℝ),
    ∏ i : ι,
      (∫⁻ (xᵢ : ℝ),
          enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
            (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i xᵢ))) ^
        (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)
Tactic: calc ∫⁻ x, ‖u x‖ₑ ^ p
      = ∫⁻ x, (‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ))) ^ (#ι : ℝ) := by
        -- a little algebraic manipulation of the exponent
        congr! 2 with x
        rw [← ENNReal.rpow_mul, hp.conjugate_eq]
        field_simp
    _ = ∫⁻ x, ∏ _i : ι, ‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ)) := by
        -- express the left-hand integrand as a product of identical factors
        congr! 2 with x
        simp_rw [prod_const]
        norm_cast
    _ ≤ ∫⁻ x, ∏ i, (∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ) ^ ((1 : ℝ) / (#ι - 1 : ℝ)) := ?_
    _ ≤ (∫⁻ x, ‖fderiv ℝ u x‖ₑ) ^ p := by
        -- apply the grid-lines lemma
        apply lintegral_prod_lintegral_pow_le _ hp
        fun_prop