Theorem: Minimum.submean (Ray/Hartogs/Subharmonic.lean)

State before:
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
Tactic:
rcases Metric.isOpen_iff.mp isOpen_interior c cs with ⟨r, rp, rs⟩
State after:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)

State before:
case intro.intro
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
Tactic:
use r, rp
State after:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
⊢ ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)

State before:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
⊢ ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
Tactic:
intro t tp tr
State after:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
⊢ f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)

State before:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
⊢ f c ≤ ⨍ (t_1 : ℝ) in itau, f (circleMap c t t_1)
Tactic:
rw [average_eq]
State after:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)

State before:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)
Tactic:
have fg : ∀ (u) (_ : u ∈ itau), f c ≤ f (circleMap c t u) := fun _ _ ↦ fm _
State after:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)

State before:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)
Tactic:
have ss : closedBall c t ⊆ s :=
  _root_.trans (Metric.closedBall_subset_ball tr) (_root_.trans rs interior_subset)
State after:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
ss : closedBall c t ⊆ s
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)

State before:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
ss : closedBall c t ⊆ s
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)
Tactic:
have n := NiceVolume.itau
State after:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
ss : closedBall c t ⊆ s
n : NiceVolume itau
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)

State before:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
ss : closedBall c t ⊆ s
n : NiceVolume itau
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)
Tactic:
have m := setIntegral_ge_of_const_le n.measurable n.ne_top fg
  ((fc.mono ss).integrableOn_sphere tp)
State after:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
ss : closedBall c t ⊆ s
n : NiceVolume itau
m : f c * (↑volume itau).toReal ≤ ∫ (x : ℝ) in itau, f (circleMap c t x)
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)

State before:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
ss : closedBall c t ⊆ s
n : NiceVolume itau
m : f c * (↑volume itau).toReal ≤ ∫ (x : ℝ) in itau, f (circleMap c t x)
⊢ f c ≤ (↑(volume.restrict itau) univ).toReal⁻¹ • ∫ (x : ℝ) in itau, f (circleMap c t x)
Tactic:
simp only [MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, smul_eq_mul, ge_iff_le]
State after:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
ss : closedBall c t ⊆ s
n : NiceVolume itau
m : f c * (↑volume itau).toReal ≤ ∫ (x : ℝ) in itau, f (circleMap c t x)
⊢ f c ≤ (↑volume itau).toReal⁻¹ * ∫ (x : ℝ) in itau, f (circleMap c t x)

State before:
case right
S : Type
inst✝¹⁵ : RCLike S
inst✝¹⁴ : SMulCommClass ℝ S S
T : Type
inst✝¹³ : RCLike T
inst✝¹² : SMulCommClass ℝ T T
E : Type
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : CompleteSpace E
inst✝⁹ : NormedSpace ℝ E
F : Type
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace ℝ F
H : Type
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : CompleteSpace H
inst✝³ : NormedSpace ℂ H
inst✝² : SecondCountableTopology E
inst✝¹ : SecondCountableTopology F
inst✝ : SecondCountableTopology H
f : ℂ → ℝ
s : Set ℂ
c : ℂ
fc : ContinuousOn f s
cs : c ∈ interior s
fm : ∀ (z : ℂ), f c ≤ f z
r : ℝ
rp : r > 0
rs : ball c r ⊆ interior s
t : ℝ
tp : 0 < t
tr : t < r
fg : ∀ u ∈ itau, f c ≤ f (circleMap c t u)
ss : closedBall c t ⊆ s
n : NiceVolume itau
m : f c * (↑volume itau).toReal ≤ ∫ (x : ℝ) in itau, f (circleMap c t x)
⊢ f c ≤ (↑volume itau).toReal⁻¹ * ∫ (x : ℝ) in itau, f (circleMap c t x)
Tactic:
simpa only [mul_comm, ← div_eq_mul_inv, le_div_iff n.real_pos]
State after:
no goals