-- Mathlib/Topology/MetricSpace/HolderNorm.lean
lemma MemHolder.holderWith {r : ℝ≥0} {f : X → Y} (hf : MemHolder r f) :
    HolderWith (nnHolderNorm r f) r f

Proof state:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
h₂ : edist x₁ x₂ ^ ↑r ≠ ⊤
C : ℝ≥0
hC : HolderWith C r f
⊢ edist (f x₁) (f x₂) / edist x₁ x₂ ^ ↑r ≤ ↑C

Tactic:
rw [ENNReal.div_le_iff h₁ h₂]

Result:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
h₂ : edist x₁ x₂ ^ ↑r ≠ ⊤
C : ℝ≥0
hC : HolderWith C r f
⊢ edist (f x₁) (f x₂) ≤ ↑C * edist x₁ x₂ ^ ↑r

Proof state:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
h₂ : edist x₁ x₂ ^ ↑r ≠ ⊤
⊢ edist (f x₁) (f x₂) ≤ (⨅ C, ⨅ (_ : HolderWith C r f), ↑C) * edist x₁ x₂ ^ ↑r

Tactic:
rw [← ENNReal.div_le_iff h₁ h₂]

Result:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
h₂ : edist x₁ x₂ ^ ↑r ≠ ⊤
⊢ edist (f x₁) (f x₂) / edist x₁ x₂ ^ ↑r ≤ ⨅ C, ⨅ (_ : HolderWith C r f), ↑C

Proof state:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
h₂ : edist x₁ x₂ ^ ↑r ≠ ⊤
⊢ edist (f x₁) (f x₂) / edist x₁ x₂ ^ ↑r ≤ ⨅ C, ⨅ (_ : HolderWith C r f), ↑C

Tactic:
refine le_iInf₂ fun C hC => ?_

Result:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
h₂ : edist x₁ x₂ ^ ↑r ≠ ⊤
C : ℝ≥0
hC : HolderWith C r f
⊢ edist (f x₁) (f x₂) / edist x₁ x₂ ^ ↑r ≤ ↑C

Proof state:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
h₂ : edist x₁ x₂ ^ ↑r ≠ ⊤
C : ℝ≥0
hC : HolderWith C r f
⊢ edist (f x₁) (f x₂) ≤ ↑C * edist x₁ x₂ ^ ↑r

Tactic:
exact hC x₁ x₂

Result:
no goals

Proof state:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ edist (f x₁) (f x₂) ≤ (⨅ C, ⨅ (_ : HolderWith C r f), ↑C) * edist x₁ x₂ ^ ↑r

case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ ⨅ C, ⨅ (_ : HolderWith C r f), ↑C ≠ ⊤

Tactic:
on_goal 2 => exact hf.eHolderNorm_lt_top.ne

Result:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ edist (f x₁) (f x₂) ≤ (⨅ C, ⨅ (_ : HolderWith C r f), ↑C) * edist x₁ x₂ ^ ↑r

Proof state:
case pos
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : x₁ = x₂
⊢ edist (f x₁) (f x₂) ≤ ↑(nnHolderNorm r f) * edist x₁ x₂ ^ ↑r

Tactic:
simp only [hx, edist_self, zero_le]

Result:
no goals

Proof state:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ edist (f x₁) (f x₂) ≤ ↑(nnHolderNorm r f) * edist x₁ x₂ ^ ↑r

Tactic:
rw [nnHolderNorm, eHolderNorm, coe_toNNReal]

Result:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ edist (f x₁) (f x₂) ≤ (⨅ C, ⨅ (_ : HolderWith C r f), ↑C) * edist x₁ x₂ ^ ↑r

case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ ⨅ C, ⨅ (_ : HolderWith C r f), ↑C ≠ ⊤

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
⊢ HolderWith (nnHolderNorm r f) r f

Tactic:
intros x₁ x₂

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
⊢ edist (f x₁) (f x₂) ≤ ↑(nnHolderNorm r f) * edist x₁ x₂ ^ ↑r

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
⊢ edist (f x₁) (f x₂) ≤ ↑(nnHolderNorm r f) * edist x₁ x₂ ^ ↑r

Tactic:
by_cases hx : x₁ = x₂

Result:
case pos
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : x₁ = x₂
⊢ edist (f x₁) (f x₂) ≤ ↑(nnHolderNorm r f) * edist x₁ x₂ ^ ↑r

case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ edist (f x₁) (f x₂) ≤ ↑(nnHolderNorm r f) * edist x₁ x₂ ^ ↑r

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
⊢ edist x₁ x₂ ^ ↑r ≠ ⊤

Tactic:
simp [(edist_lt_top x₁ x₂).ne]

Result:
no goals

Proof state:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
⊢ edist (f x₁) (f x₂) ≤ (⨅ C, ⨅ (_ : HolderWith C r f), ↑C) * edist x₁ x₂ ^ ↑r

Tactic:
have h₂ : edist x₁ x₂ ^ (r : ℝ) ≠ ∞ := by
  simp [(edist_lt_top x₁ x₂).ne]

Result:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
h₂ : edist x₁ x₂ ^ ↑r ≠ ⊤
⊢ edist (f x₁) (f x₂) ≤ (⨅ C, ⨅ (_ : HolderWith C r f), ↑C) * edist x₁ x₂ ^ ↑r

Proof state:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ edist (f x₁) (f x₂) ≤ (⨅ C, ⨅ (_ : HolderWith C r f), ↑C) * edist x₁ x₂ ^ ↑r

Tactic:
have h₁ : edist x₁ x₂ ^ (r : ℝ) ≠ 0 :=
  (Ne.symm <| ne_of_lt <| ENNReal.rpow_pos (edist_pos.2 hx) (edist_lt_top x₁ x₂).ne)

Result:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
h₁ : edist x₁ x₂ ^ ↑r ≠ 0
⊢ edist (f x₁) (f x₂) ≤ (⨅ C, ⨅ (_ : HolderWith C r f), ↑C) * edist x₁ x₂ ^ ↑r

Proof state:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
hf : MemHolder r f
x₁ x₂ : X
hx : ¬x₁ = x₂
⊢ ⨅ C, ⨅ (_ : HolderWith C r f), ↑C ≠ ⊤

Tactic:
exact hf.eHolderNorm_lt_top.ne

Result:
no goals