diff --git a/Nevanlinna/stronglyMeromorphic_JensenFormula.lean b/Nevanlinna/stronglyMeromorphic_JensenFormula.lean
index 23bb8df..3ace982 100644
--- a/Nevanlinna/stronglyMeromorphic_JensenFormula.lean
+++ b/Nevanlinna/stronglyMeromorphic_JensenFormula.lean
@@ -11,28 +11,30 @@ import Nevanlinna.meromorphicOn_divisor
 open Real
 
 
-
-theorem jensen_case_R_eq_one'
+theorem jensen
+  {R : ℝ}
+  (hR : 0 < R)
   (f : ℂ → ℂ)
-  (h₁f : StronglyMeromorphicOn f (Metric.closedBall 0 1))
+  (h₁f : StronglyMeromorphicOn f (Metric.closedBall 0 R))
   (h₂f : f 0 ≠ 0) :
-  log ‖f 0‖ = -∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log (‖s‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 1 x)‖ := by
+  log ‖f 0‖ = -∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log (R * ‖s‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 R x)‖ := by
 
-  have h₁U : IsConnected (Metric.closedBall (0 : ℂ) 1) := by
+  have h₁U : IsConnected (Metric.closedBall (0 : ℂ) R) := by
     constructor
-    · apply Metric.nonempty_closedBall.mpr (by simp)
-    · exact (convex_closedBall (0 : ℂ) 1).isPreconnected
+    · apply Metric.nonempty_closedBall.mpr
+      exact le_of_lt hR
+    · exact (convex_closedBall (0 : ℂ) R).isPreconnected
 
-  have h₂U : IsCompact (Metric.closedBall (0 : ℂ) 1) :=
-    isCompact_closedBall 0 1
+  have h₂U : IsCompact (Metric.closedBall (0 : ℂ) R) :=
+    isCompact_closedBall 0 R
 
-  have h'₂f : ∃ u : (Metric.closedBall (0 : ℂ) 1), f u ≠ 0 := by
-    use ⟨0, Metric.mem_closedBall_self (by simp)⟩
+  have h'₂f : ∃ u : (Metric.closedBall (0 : ℂ) R), f u ≠ 0 := by
+    use ⟨0, Metric.mem_closedBall_self (le_of_lt hR)⟩
 
   have h₃f : Set.Finite (Function.support h₁f.meromorphicOn.divisor) := by
     exact Divisor.finiteSupport h₂U (StronglyMeromorphicOn.meromorphicOn h₁f).divisor
 
-  have h₄f: Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log (‖s‖⁻¹)) ⊆ h₃f.toFinset := by
+  have h₄f: Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log (R * ‖s‖⁻¹)) ⊆ h₃f.toFinset := by
     intro x
     contrapose
     simp
@@ -63,7 +65,7 @@ theorem jensen_case_R_eq_one'
     rw [hs]
     simp
 
-  have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) 1, f z ≠ 0 → log ‖f z‖ = G z := by
+  have decompose_f : ∀ z ∈ Metric.closedBall (0 : ℂ) R, f z ≠ 0 → log ‖f z‖ = G z := by
     intro z h₁z h₂z
 
     rw [h₄F]
@@ -104,40 +106,41 @@ theorem jensen_case_R_eq_one'
     simpa
 
 
-  have int_logAbs_f_eq_int_G : ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 1 x)‖ = ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x) := by
+  have int_logAbs_f_eq_int_G : ∫ (x : ℝ) in (0)..2 * π, log ‖f (circleMap 0 R x)‖ = ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 R x) := by
 
     rw [intervalIntegral.integral_congr_ae]
     rw [MeasureTheory.ae_iff]
     apply Set.Countable.measure_zero
     simp
 
-    have t₀ : {a | a ∈ Ι 0 (2 * π) ∧ ¬log ‖f (circleMap 0 1 a)‖ = G (circleMap 0 1 a)}
-      ⊆ (circleMap 0 1)⁻¹' (h₃f.toFinset) := by
+    have t₀ : {a | a ∈ Ι 0 (2 * π) ∧ ¬log ‖f (circleMap 0 R a)‖ = G (circleMap 0 R a)}
+      ⊆ (circleMap 0 R)⁻¹' (h₃f.toFinset) := by
       intro a ha
       simp at ha
       simp
       by_contra C
-      have t₀ : (circleMap 0 1 a) ∈ Metric.closedBall 0 1 :=
-        circleMap_mem_closedBall 0 (zero_le_one' ℝ) a
-      have t₁ : f (circleMap 0 1 a) ≠ 0 := by
-        let A := h₁f (circleMap 0 1 a) t₀
+      have t₀ : (circleMap 0 R a) ∈ Metric.closedBall 0 R := by
+        apply circleMap_mem_closedBall
+        exact le_of_lt hR
+      have t₁ : f (circleMap 0 R a) ≠ 0 := by
+        let A := h₁f (circleMap 0 R a) t₀
         rw [← A.order_eq_zero_iff]
         unfold MeromorphicOn.divisor at C
         simp [t₀] at C
         rcases C with C₁|C₂
         · assumption
         · let B := h₁f.meromorphicOn.order_ne_top' h₁U
-          let C := fun q ↦ B q ⟨(circleMap 0 1 a), t₀⟩
+          let C := fun q ↦ B q ⟨(circleMap 0 R a), t₀⟩
           rw [C₂] at C
-          have : ∃ u : (Metric.closedBall (0 : ℂ) 1), (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by
-            use ⟨(0 : ℂ), (by simp)⟩
-            let H := h₁f 0 (by simp)
+          have : ∃ u : (Metric.closedBall (0 : ℂ) R), (h₁f u u.2).meromorphicAt.order ≠ ⊤ := by
+            use ⟨(0 : ℂ), (by simp; exact le_of_lt hR)⟩
+            let H := h₁f 0 (by simp; exact le_of_lt hR)
             let K := H.order_eq_zero_iff.2 h₂f
             rw [K]
             simp
           let D := C this
           tauto
-      exact ha.2 (decompose_f (circleMap 0 1 a) t₀ t₁)
+      exact ha.2 (decompose_f (circleMap 0 R a) t₀ t₁)
 
     apply Set.Countable.mono t₀
     apply Set.Countable.preimage_circleMap
@@ -147,14 +150,14 @@ theorem jensen_case_R_eq_one'
     simp
 
 
-  have decompose_int_G : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 1 x)
-    = (∫ (x : ℝ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 1 x))))
-        + ∑ᶠ x, (h₁f.meromorphicOn.divisor x) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - ↑x)) := by
+  have decompose_int_G : ∫ (x : ℝ) in (0)..2 * π, G (circleMap 0 R x)
+    = (∫ (x : ℝ) in (0)..2 * π, log (Complex.abs (F (circleMap 0 R x))))
+        + ∑ᶠ x, (h₁f.meromorphicOn.divisor x) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 R x_1 - ↑x)) := by
     dsimp [G]
 
     rw [intervalIntegral.integral_add]
     congr
-    have t₀ {x : ℝ} : Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log (Complex.abs (circleMap 0 1 x - s))) ⊆ h₃f.toFinset := by
+    have t₀ {x : ℝ} : Function.support (fun s ↦ (h₁f.meromorphicOn.divisor s) * log (Complex.abs (circleMap 0 R x - s))) ⊆ h₃f.toFinset := by
       intro s hs
       simp at hs
       simp [hs.1]
@@ -164,8 +167,8 @@ theorem jensen_case_R_eq_one'
       intro x
       rw [finsum_eq_sum_of_support_subset _ t₀]
     rw [intervalIntegral.integral_finset_sum]
-    let G' := fun x ↦ ((h₁f.meromorphicOn.divisor x) : ℂ) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - x))
-    have t₁ : (Function.support fun x ↦ (h₁f.meromorphicOn.divisor x) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 1 x_1 - x))) ⊆ h₃f.toFinset := by
+    let G' := fun x ↦ ((h₁f.meromorphicOn.divisor x) : ℂ) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 R x_1 - x))
+    have t₁ : (Function.support fun x ↦ (h₁f.meromorphicOn.divisor x) * ∫ (x_1 : ℝ) in (0)..2 * π, log (Complex.abs (circleMap 0 R x_1 - x))) ⊆ h₃f.toFinset := by
       simp
       intro s
       contrapose!
@@ -182,14 +185,15 @@ theorem jensen_case_R_eq_one'
     intro i _
     apply IntervalIntegrable.const_mul
     --simp at this
-    by_cases h₂i : ‖i‖ = 1
+    by_cases h₂i : ‖i‖ = R
     -- case pos
-    exact int'₂ h₂i
+    sorry
+    --exact int'₂ h₂i
     -- case neg
     apply Continuous.intervalIntegrable
     apply continuous_iff_continuousAt.2
     intro x
-    have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑i) :=
+    have : (fun x => log (Complex.abs (circleMap 0 R x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 R x - ↑i) :=
       rfl
     rw [this]
     apply ContinuousAt.comp
@@ -201,9 +205,10 @@ theorem jensen_case_R_eq_one'
       arg 1
       rw [← ha']
       rw [Complex.norm_eq_abs]
-      rw [abs_circleMap_zero 1 x]
+      rw [abs_circleMap_zero R x]
       simp
-    tauto
+    linarith
+    --
     apply ContinuousAt.comp
     apply Complex.continuous_abs.continuousAt
     fun_prop
@@ -211,13 +216,18 @@ theorem jensen_case_R_eq_one'
     apply Continuous.intervalIntegrable
     apply continuous_iff_continuousAt.2
     intro x
-    have : (fun x => log (Complex.abs (F (circleMap 0 1 x)))) = log ∘ Complex.abs ∘ F ∘ (fun x ↦ circleMap 0 1 x) :=
+    have : (fun x => log (Complex.abs (F (circleMap 0 R x)))) = log ∘ Complex.abs ∘ F ∘ (fun x ↦ circleMap 0 R x) :=
       rfl
     rw [this]
     apply ContinuousAt.comp
     apply Real.continuousAt_log
     simp
-    exact h₃F ⟨(circleMap 0 1 x), (by simp)⟩
+    have : (circleMap 0 R x) ∈ (Metric.closedBall 0 R) := by
+      simp
+      rw [abs_le]
+      simp [hR]
+      exact le_of_lt hR
+    exact h₃F ⟨(circleMap 0 R x), this⟩
 
     -- ContinuousAt (⇑Complex.abs ∘ F ∘ fun x => circleMap 0 1 x) x
     apply ContinuousAt.comp
@@ -225,7 +235,8 @@ theorem jensen_case_R_eq_one'
     apply ContinuousAt.comp
     apply DifferentiableAt.continuousAt (𝕜 := ℂ)
     apply AnalyticAt.differentiableAt
-    exact h₂F (circleMap 0 1 x) (by simp)
+    apply h₂F (circleMap 0 R x)
+    simp; rw [abs_le]; simp [hR]; exact le_of_lt hR
     -- ContinuousAt (fun x => circleMap 0 1 x) x
     apply Continuous.continuousAt
     apply continuous_circleMap
@@ -245,15 +256,16 @@ theorem jensen_case_R_eq_one'
     apply IntervalIntegrable.const_mul
     --have : i.1 ∈ Metric.closedBall (0 : ℂ) 1 := i.2
     --simp at this
-    by_cases h₂i : ‖i‖ = 1
+    by_cases h₂i : ‖i‖ = R
     -- case pos
-    exact int'₂ h₂i
+    --exact int'₂ h₂i
+    sorry
     -- case neg
     --have : i.1 ∈ Metric.ball (0 : ℂ) 1 := by sorry
     apply Continuous.intervalIntegrable
     apply continuous_iff_continuousAt.2
     intro x
-    have : (fun x => log (Complex.abs (circleMap 0 1 x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 1 x - ↑i) :=
+    have : (fun x => log (Complex.abs (circleMap 0 R x - ↑i))) = log ∘ Complex.abs ∘ (fun x ↦ circleMap 0 R x - ↑i) :=
       rfl
     rw [this]
     apply ContinuousAt.comp
@@ -265,33 +277,34 @@ theorem jensen_case_R_eq_one'
       arg 1
       rw [← ha']
       rw [Complex.norm_eq_abs]
-      rw [abs_circleMap_zero 1 x]
+      rw [abs_circleMap_zero R x]
       simp
-    tauto
+    linarith
     apply ContinuousAt.comp
     apply Complex.continuous_abs.continuousAt
     fun_prop
 
-  have t₁ : (∫ (x : ℝ) in (0)..2 * Real.pi, log ‖F (circleMap 0 1 x)‖) = 2 * Real.pi * log ‖F 0‖ := by
+  have t₁ : (∫ (x : ℝ) in (0)..2 * Real.pi, log ‖F (circleMap 0 R x)‖) = 2 * Real.pi * log ‖F 0‖ := by
     let logAbsF := fun w ↦ Real.log ‖F w‖
-    have t₀ : ∀ z ∈ Metric.closedBall 0 1, HarmonicAt logAbsF z := by
+    have t₀ : ∀ z ∈ Metric.closedBall 0 R, HarmonicAt logAbsF z := by
       intro z hz
       apply logabs_of_holomorphicAt_is_harmonic
       exact AnalyticAt.holomorphicAt (h₂F z hz)
       exact h₃F ⟨z, hz⟩
 
-    apply harmonic_meanValue₁ 1 Real.zero_lt_one t₀
+    apply harmonic_meanValue₁ R hR t₀
+
 
   simp_rw [← Complex.norm_eq_abs] at decompose_int_G
   rw [t₁] at decompose_int_G
 
 
-  have h₁G' : (Function.support fun s => (h₁f.meromorphicOn.divisor s) * ∫ (x_1 : ℝ) in (0)..(2 * π), log ‖circleMap 0 1 x_1 - s‖) ⊆ ↑h₃f.toFinset := by
+  have h₁G' : (Function.support fun s => (h₁f.meromorphicOn.divisor s) * ∫ (x_1 : ℝ) in (0)..(2 * π), log ‖circleMap 0 R x_1 - s‖) ⊆ ↑h₃f.toFinset := by
     intro s hs
     simp at hs
     simp [hs.1]
   rw [finsum_eq_sum_of_support_subset _ h₁G'] at decompose_int_G
-  have : ∑ s ∈ h₃f.toFinset, (h₁f.meromorphicOn.divisor s) * ∫ (x_1 : ℝ) in (0)..(2 * π), log ‖circleMap 0 1 x_1 - s‖ = 0 := by
+  have : ∑ s ∈ h₃f.toFinset, (h₁f.meromorphicOn.divisor s) * ∫ (x_1 : ℝ) in (0)..(2 * π), log ‖circleMap 0 R x_1 - s‖ = 0 := by
     apply Finset.sum_eq_zero
     intro x hx
     rw [int₃ _]
@@ -359,170 +372,3 @@ theorem jensen_case_R_eq_one'
   rw [h₂f] at hx
   tauto
   assumption
-
-
-
-lemma const_mul_circleMap_zero'
-  {R θ : ℝ} :
-  circleMap 0 R θ = R * circleMap 0 1 θ := by
-  rw [circleMap_zero, circleMap_zero]
-  simp
-
-
-
-theorem jensen'
-  {R : ℝ}
-  (hR : 0 < R)
-  (f : ℂ → ℂ)
-  (h₁f : StronglyMeromorphicOn f (Metric.closedBall 0 R))
-  (h₂f : f 0 ≠ 0) :
-  log ‖f 0‖ = -∑ᶠ s, (h₁f.meromorphicOn.divisor s) * log (R * ‖s‖⁻¹) + (2 * π)⁻¹ * ∫ (x : ℝ) in (0)..(2 * π), log ‖f (circleMap 0 R x)‖ := by
-
-
-  let ℓ : ℂ ≃L[ℂ] ℂ :=
-  {
-    toFun := fun x ↦ R * x
-    map_add' := fun x y => DistribSMul.smul_add R x y
-    map_smul' := fun m x => mul_smul_comm m (↑R) x
-    invFun := fun x ↦ R⁻¹ * x
-    left_inv := by
-      intro x
-      simp
-      rw [← mul_assoc, mul_comm, inv_mul_cancel₀, mul_one]
-      simp
-      exact ne_of_gt hR
-    right_inv := by
-      intro x
-      simp
-      rw [← mul_assoc, mul_inv_cancel₀, one_mul]
-      simp
-      exact ne_of_gt hR
-    continuous_toFun := continuous_const_smul R
-    continuous_invFun := continuous_const_smul R⁻¹
-  }
-
-
-  let F := f ∘ ℓ
-
-  have h₁F : StronglyMeromorphicOn F (Metric.closedBall 0 1) := by
-    sorry
-/-
-    apply AnalyticOnNhd.comp (t := Metric.closedBall 0 R)
-    exact h₁f
-    intro x _
-    apply ℓ.toContinuousLinearMap.analyticAt x
-
-    intro x hx
-    have : ℓ x = R * x := by rfl
-    rw [this]
-    simp
-    simp at hx
-    rw [abs_of_pos hR]
-    calc R * Complex.abs x
-    _ ≤ R * 1 := by exact (mul_le_mul_iff_of_pos_left hR).mpr hx
-    _ = R := by simp
--/
-  have h₂F : F 0 ≠ 0 := by
-    dsimp [F]
-    have : ℓ 0 = R * 0 := by rfl
-    rw [this]
-    simpa
-
-  let A := jensen_case_R_eq_one' F h₁F h₂F
-
-  dsimp [F] at A
-  have {x : ℂ} : ℓ x = R * x := by rfl
-  repeat
-    simp_rw [this] at A
-  simp at A
-  simp
-  rw [A]
-  simp_rw [← const_mul_circleMap_zero']
-  simp
-
-  let e : (Metric.closedBall (0 : ℂ) 1) → (Metric.closedBall (0 : ℂ) R) := by
-    intro ⟨x, hx⟩
-    have hy : R • x ∈ Metric.closedBall (0 : ℂ) R := by
-      simp
-      simp at hx
-      have : R = |R| := by exact Eq.symm (abs_of_pos hR)
-      rw [← this]
-      norm_num
-      calc R * Complex.abs x
-      _ ≤ R * 1 := by exact (mul_le_mul_iff_of_pos_left hR).mpr hx
-      _ = R := by simp
-    exact ⟨R • x, hy⟩
-
-  let e' : (Metric.closedBall (0 : ℂ) R) → (Metric.closedBall (0 : ℂ) 1) := by
-    intro ⟨x, hx⟩
-    have hy : R⁻¹ • x ∈ Metric.closedBall (0 : ℂ) 1 := by
-      simp
-      simp at hx
-      have : R = |R| := by exact Eq.symm (abs_of_pos hR)
-      rw [← this]
-      norm_num
-      calc R⁻¹ * Complex.abs x
-      _ ≤ R⁻¹ * R := by
-        apply mul_le_mul_of_nonneg_left hx
-        apply inv_nonneg.mpr
-        exact abs_eq_self.mp (id (Eq.symm this))
-      _ = 1 := by
-        apply inv_mul_cancel₀
-        exact Ne.symm (ne_of_lt hR)
-    exact ⟨R⁻¹ • x, hy⟩
-
-  apply finsum_eq_of_bijective e
-
-
-  apply Function.bijective_iff_has_inverse.mpr
-  use e'
-  constructor
-  · apply Function.leftInverse_iff_comp.mpr
-    funext x
-    dsimp only [e, e',  id_eq, eq_mp_eq_cast, Function.comp_apply]
-    conv =>
-      left
-      arg 1
-      rw [← smul_assoc, smul_eq_mul]
-      rw [inv_mul_cancel₀ (Ne.symm (ne_of_lt hR))]
-      rw [one_smul]
-  · apply Function.rightInverse_iff_comp.mpr
-    funext x
-    dsimp only [e, e',  id_eq, eq_mp_eq_cast, Function.comp_apply]
-    conv =>
-      left
-      arg 1
-      rw [← smul_assoc, smul_eq_mul]
-      rw [mul_inv_cancel₀ (Ne.symm (ne_of_lt hR))]
-      rw [one_smul]
-
-  intro x
-  simp
-  by_cases hx : x = (0 : ℂ)
-  rw [hx]
-  simp
-
-  rw [log_mul, log_mul, log_inv, log_inv]
-  have : R = |R| := by exact Eq.symm (abs_of_pos hR)
-  rw [← this]
-  simp
-  left
-  congr 1
-
-  dsimp [AnalyticOnNhd.order]
-  rw [← AnalyticAt.order_comp_CLE ℓ]
-
-  --
-  simpa
-  --
-  have : R = |R| := by exact Eq.symm (abs_of_pos hR)
-  rw [← this]
-  apply inv_ne_zero
-  exact Ne.symm (ne_of_lt hR)
-  --
-  exact Ne.symm (ne_of_lt hR)
-  --
-  simp
-  constructor
-  · assumption
-  · exact Ne.symm (ne_of_lt hR)