Theorem: SubharmonicOn.constMul (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 ℂ
a : ℝ
fs : SubharmonicOn f s
ap : 0 ≤ a
⊢ ∀ c ∈ interior s, ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → a * f c ≤ ⨍ (t : ℝ) in itau, a * f (circleMap c s t)
Tactic:
intro c cs
State after:
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 ℂ
a : ℝ
fs : SubharmonicOn f s
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → a * f c ≤ ⨍ (t : ℝ) in itau, a * f (circleMap c s t)

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 ℂ
a : ℝ
fs : SubharmonicOn f s
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → a * f c ≤ ⨍ (t : ℝ) in itau, a * f (circleMap c s t)
Tactic:
rcases fs.submean' c cs with ⟨r, rp, rm⟩
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 ℂ
a : ℝ
fs : SubharmonicOn f s
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s
r : ℝ
rp : 0 < r
rm : ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → a * f c ≤ ⨍ (t : ℝ) in itau, a * 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 ℂ
a : ℝ
fs : SubharmonicOn f s
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s
r : ℝ
rp : 0 < r
rm : ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ ∃ r, 0 < r ∧ ∀ (s : ℝ), 0 < s → s < r → a * f c ≤ ⨍ (t : ℝ) in itau, a * 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 ℂ
a : ℝ
fs : SubharmonicOn f s
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s
r : ℝ
rp : 0 < r
rm : ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ ∀ (s : ℝ), 0 < s → s < r → a * f c ≤ ⨍ (t : ℝ) in itau, a * 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 ℂ
a : ℝ
fs : SubharmonicOn f s
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s
r : ℝ
rp : 0 < r
rm : ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ ∀ (s : ℝ), 0 < s → s < r → a * f c ≤ ⨍ (t : ℝ) in itau, a * f (circleMap c s t)
Tactic:
intro s sp sr
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 ℂ
a : ℝ
fs : SubharmonicOn f s✝
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s✝
r : ℝ
rp : 0 < r
rm : ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
s : ℝ
sp : 0 < s
sr : s < r
⊢ a * f c ≤ ⨍ (t : ℝ) in itau, a * 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 ℂ
a : ℝ
fs : SubharmonicOn f s✝
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s✝
r : ℝ
rp : 0 < r
rm : ∀ (s : ℝ), 0 < s → s < r → f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
s : ℝ
sp : 0 < s
sr : s < r
⊢ a * f c ≤ ⨍ (t : ℝ) in itau, a * f (circleMap c s t)
Tactic:
specialize rm s sp sr
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 ℂ
a : ℝ
fs : SubharmonicOn f s✝
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s✝
r : ℝ
rp : 0 < r
s : ℝ
sp : 0 < s
sr : s < r
rm : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ a * f c ≤ ⨍ (t : ℝ) in itau, a * 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 ℂ
a : ℝ
fs : SubharmonicOn f s✝
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s✝
r : ℝ
rp : 0 < r
s : ℝ
sp : 0 < s
sr : s < r
rm : f c ≤ ⨍ (t : ℝ) in itau, f (circleMap c s t)
⊢ a * f c ≤ ⨍ (t : ℝ) in itau, a * f (circleMap c s t)
Tactic:
simp only [average_eq, MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter,
  smul_eq_mul] at rm ⊢
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 ℂ
a : ℝ
fs : SubharmonicOn f s✝
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s✝
r : ℝ
rp : 0 < r
s : ℝ
sp : 0 < s
sr : s < r
rm : f c ≤ (↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, f (circleMap c s t)
⊢ a * f c ≤ (↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, a * 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 ℂ
a : ℝ
fs : SubharmonicOn f s✝
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s✝
r : ℝ
rp : 0 < r
s : ℝ
sp : 0 < s
sr : s < r
rm : f c ≤ (↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, f (circleMap c s t)
⊢ a * f c ≤ (↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, a * f (circleMap c s t)
Tactic:
calc a * f c
  _ ≤ a * ((volume itau).toReal⁻¹ * ∫ t in itau, f (circleMap c s t)) := by bound
  _ = (volume itau).toReal⁻¹ * (a * ∫ t in itau, f (circleMap c s t)) := by ring
  _ = (volume itau).toReal⁻¹ * ∫ t in itau, a * f (circleMap c s t) := by
    rw [integral_mul_left]
State after:
no goals

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 ℂ
a : ℝ
fs : SubharmonicOn f s✝
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s✝
r : ℝ
rp : 0 < r
s : ℝ
sp : 0 < s
sr : s < r
rm : f c ≤ (↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, f (circleMap c s t)
⊢ a * f c ≤ a * ((↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, f (circleMap c s t))
Tactic:
bound
State after:
no goals

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 ℂ
a : ℝ
fs : SubharmonicOn f s✝
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s✝
r : ℝ
rp : 0 < r
s : ℝ
sp : 0 < s
sr : s < r
rm : f c ≤ (↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, f (circleMap c s t)
⊢ a * ((↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, f (circleMap c s t)) =
    (↑volume itau).toReal⁻¹ * (a * ∫ (t : ℝ) in itau, f (circleMap c s t))
Tactic:
ring
State after:
no goals

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 ℂ
a : ℝ
fs : SubharmonicOn f s✝
ap : 0 ≤ a
c : ℂ
cs : c ∈ interior s✝
r : ℝ
rp : 0 < r
s : ℝ
sp : 0 < s
sr : s < r
rm : f c ≤ (↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, f (circleMap c s t)
⊢ (↑volume itau).toReal⁻¹ * (a * ∫ (t : ℝ) in itau, f (circleMap c s t)) =
    (↑volume itau).toReal⁻¹ * ∫ (t : ℝ) in itau, a * f (circleMap c s t)
Tactic:
rw [integral_mul_left]
State after:
no goals