awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
⊢ 0 ≤ 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1

Tactic:
have h2 : 0 ≤ ((1 : ℝ) / (#ι - 1 : ℝ)) := by positivity
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
field_simp : LE.le (α := ℝ) 1 1
⊢ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) ≤ 1

Tactic:
field_simp
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
⊢ LE.le (α := ℝ) 1 1

Tactic:
rfl
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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

Tactic:
have h3 : (#ι - 1 : ℝ) * ((1 : ℝ) / (#ι - 1 : ℝ)) ≤ 1 := by field_simp; rfl
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
simp : p * HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 = (↑#ι : ℝ)
⊢ p = 1 + 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1

Tactic:
simp [field]
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 = (↑#ι : ℝ)
rw₁ rw₂ : Eq (α := ℝ) (↑#ι : ℝ) (↑#ι : ℝ)
⊢ p * HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 = (↑#ι : ℝ)

Tactic:
rw [mul_comm, hp.sub_one_mul_conj]

Premises used: mul_comm, Real.HolderConjugate.sub_one_mul_conj
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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

Tactic:
have h4 : p = 1 + 1 / (↑#ι - 1) := by simp [field]; rw [mul_comm, hp.sub_one_mul_conj]
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
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)
⊢ ∫⁻ (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

Tactic:
rw [h4]
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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),
      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) ∂Measure.pi (α := A) μ ≤
    (∫⁻ (x : (i : ι) → A i), f x ∂Measure.pi (α := A) μ) ^ (1 + 1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)

Tactic:
lintegral_mul_prod_lintegral_pow_le μ h2 h3 hf

Premises used: MeasureTheory.lintegral_mul_prod_lintegral_pow_le
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
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)
⊢ ∫⁻ (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:
convert! lintegral_mul_prod_lintegral_pow_le μ h2 h3 hf using 2

Premises used: MeasureTheory.lintegral_mul_prod_lintegral_pow_le
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
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)
⊢ 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:
field_simp
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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) ↦
      ∏ 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:
simp
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
⊢ LE.le (α := ℝ) 2 (↑#ι : ℝ)

Tactic:
exact_mod_cast hp.lt

Premises used: Real.HolderTriple.lt
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
⊢ LE.le (α := ℝ) 2 (↑#ι : ℝ)

Tactic:
have hι : (2 : ℝ) ≤ #ι := by exact_mod_cast hp.lt
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 (↑#ι : ℝ)
linarith :
  HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 < 1 → HSub.hSub (α := ℝ) 2 (↑#ι : ℝ) + (HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 - 1) = 0
⊢ 1 ≤ HSub.hSub (α := ℝ) (↑#ι : ℝ) 1

Tactic:
linarith
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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

Tactic:
have : (1 : ℝ) ≤ ↑#ι - 1 := by
    have hι : (2 : ℝ) ≤ #ι := by exact_mod_cast hp.lt
    linarith
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
h : ∀ (x : ι → ℝ), ‖u x‖ₑ ^ p = HPow.hPow (β := ℝ) (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) (↑#ι : ℝ)
⊢ ∫⁻ (x : ι → ℝ), ‖u x‖ₑ ^ p =
    ∫⁻ (x : ι → ℝ), HPow.hPow (β := ℝ) (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) (↑#ι : ℝ)

Tactic:
congr! 2 with x
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : ι → ℝ
h : ‖u x‖ₑ ^ ((↑#ι : ℝ) / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) = ‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * (↑#ι : ℝ))
⊢ ‖u x‖ₑ ^ p = HPow.hPow (β := ℝ) (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) (↑#ι : ℝ)

Tactic:
rw [← ENNReal.rpow_mul, hp.conjugate_eq]

Premises used: ENNReal.rpow_mul, Real.HolderConjugate.conjugate_eq
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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‖ₑ ^ ((↑#ι : ℝ) / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1) = ‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1 * (↑#ι : ℝ))

Tactic:
field_simp
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
h :
  ∀ (x : ι → ℝ),
    HPow.hPow (β := ℝ) (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) (↑#ι : ℝ) =
      ∏ _i : ι, ‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)
⊢ ∫⁻ (x : ι → ℝ), HPow.hPow (β := ℝ) (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) (↑#ι : ℝ) =
    ∫⁻ (x : ι → ℝ), ∏ _i : ι, ‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)

Tactic:
congr! 2 with x
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : ι → ℝ
h :
  HPow.hPow (β := ℝ) (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) (↑#ι : ℝ) =
    (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) ^ card.{u_1} (α := ι) Finset.univ
⊢ HPow.hPow (β := ℝ) (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) (↑#ι : ℝ) =
    ∏ _i : ι, ‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)

Tactic:
simp_rw [prod_const]

Premises used: Finset.prod_const
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : ι → ℝ
h h₁ h₂ 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
⊢ HPow.hPow (β := ℝ) (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) (↑#ι : ℝ) =
    (‖u x‖ₑ ^ (1 / HSub.hSub (α := ℝ) (↑#ι : ℝ) 1)) ^ card.{u_1} (α := ι) Finset.univ

Tactic:
norm_cast
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : ι → ℝ), ∏ _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:
?_
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
apply :
  Measurable (β := ℝ≥0∞) fun (x : (i : ι) → ℝ) ↦
    enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F) (fderiv ℝ u x)
⊢ ∫⁻ (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

Tactic:
apply lintegral_prod_lintegral_pow_le _ hp

Premises used: MeasureTheory.lintegral_prod_lintegral_pow_le
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : ι) ↦ ℝ))
funProp₂ :
  MeasurableEmbedding (β := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F) fun (x : (i : ι) → ℝ) ↦
    fderiv ℝ u x
⊢ Measurable (β := ℝ≥0∞) fun (x : (i : ι) → ℝ) ↦
    enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F) (fderiv ℝ u x)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
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)
⊢ ∫⁻ (x : ι → ℝ), ‖u x‖ₑ ^ p ≤
    (∫⁻ (x : ι → ℝ), enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F) (fderiv ℝ u x)) ^ p

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

Premises used: Real, HSub.hSub, Fintype.card, HDiv.hDiv, fderiv, Nat.cast, ENorm.enorm, MeasureTheory.MeasureSpace.volume, OfNat.ofNat, MeasureTheory.lintegral
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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
hfg :
  ∀ (x : ι → ℝ) (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      ‖u x‖ₑ ≤
        ∫⁻ (xᵢ : ℝ),
          enorm (E := ContinuousLinearMap.{0, 0, u_1, u_3} (RingHom.id ℝ) (ι → ℝ) F)
            (fderiv ℝ u (update (β := fun (a : ι) ↦ ℝ) x i xᵢ))
⊢ ∫⁻ (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:
gcongr with x i
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ ‖u x‖ₑ ≤ ‖(u ∘ update (β := fun (a : ι) ↦ ℝ) x i) (x i)‖ₑ

Tactic:
simp
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
apply : ContDiff ℝ 1 (u ∘ update (β := fun (a : ι) ↦ ℝ) x i)
apply₁ : HasCompactSupport (u ∘ update (β := fun (a : ι) ↦ ℝ) x i)
⊢ ‖u x‖ₑ ≤ ∫⁻ (xᵢ : ℝ) in Set.Iic (x i), ‖deriv (u ∘ update (β := fun (a : ι) ↦ ℝ) x i) xᵢ‖ₑ

Tactic:
apply le_trans (by simp) (HasCompactSupport.enorm_le_lintegral_Ici_deriv _ _ _)

Premises used: HasCompactSupport.enorm_le_lintegral_Ici_deriv, le_trans
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ ContDiff ℝ 1 (update (β := fun (i : ι) ↦ ℝ) x i)

Tactic:
contDiff_update 1 x i

Premises used: contDiff_update, OfNat.ofNat
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ ContDiff ℝ 1 (update (β := fun (a : ι) ↦ ℝ) x i)

Tactic:
convert! contDiff_update 1 x i

Premises used: contDiff_update, OfNat.ofNat
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ ContDiff ℝ 1 (u ∘ update (β := fun (a : ι) ↦ ℝ) x i)

Tactic:
exact hu.comp (by convert! contDiff_update 1 x i)

Premises used: ContDiff.comp
-- Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality
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 : ι → ℝ
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ HasCompactSupport (u ∘ update (β := fun (a : ι) ↦ ℝ) x i)

Tactic:
h2u.comp_isClosedEmbedding (isClosedEmbedding_update x i)

Premises used: HasCompactSupport.comp_isClosedEmbedding, isClosedEmbedding_update