pith. machine review for the scientific record. sign in
theorem proved tactic proof

measurement_bridge_C_eq_2A

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 152theorem measurement_bridge_C_eq_2A (rot : TwoBranchRotation) :
 153  pathAction (pathFromRotation rot) = 2 * rateAction rot := by

proof body

Tactic-mode proof.

 154  unfold pathAction pathFromRotation rateAction
 155  simp
 156  have hkernel : ∫ ϑ in (0)..(π/2 - rot.θ_s),
 157                   Jcost (recognitionProfile (ϑ + rot.θ_s)) =
 158                2 * ∫ ϑ in (0)..(π/2 - rot.θ_s), Real.cot (ϑ + rot.θ_s) :=
 159    kernel_integral_match rot.θ_s rot.θ_s_bounds
 160  rw [hkernel]
 161  have h_subst :
 162      ∫ ϑ in (0)..(π/2 - rot.θ_s), Real.cot (ϑ + rot.θ_s)
 163        = ∫ θ in rot.θ_s..(π/2), Real.cot θ := by
 164    simpa [sub_eq_add_neg, add_comm, add_left_comm, add_assoc]
 165      using
 166        (intervalIntegral.integral_comp_add_right
 167          (a := (0 : ℝ)) (b := π/2 - rot.θ_s)
 168          (f := fun θ => Real.cot θ) (d := rot.θ_s))
 169  have hI := integral_cot_from_theta rot.θ_s rot.θ_s_bounds
 170  have htan :
 171      ∫ ϑ in (0)..(π/2 - rot.θ_s), Real.cot (ϑ + rot.θ_s)
 172        = - Real.log (Real.sin rot.θ_s) := by
 173    simpa [h_subst] using hI
 174  simp [htan, two_mul, mul_left_comm, mul_assoc]
 175
 176/-- Weight bridge: w = exp(-C) = exp(-2A) -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (14)

Lean names referenced from this declaration's body.