Theorem: circleParam.arg_θ.jacobian_rule (test/prob_ad/circle_discont_2d.lean)

State before:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ jacobian R circleParam = 1
Tactic:
unfold circleParam jacobian
State after:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x =>
      let dg := ∂ (θ:=x), (cos θ, sin θ);
      let dg' := semiAdjoint R dg;
      sqrt (det R (dg' ∘ dg))) =
    1

State before:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x =>
      let dg := ∂ (θ:=x), (cos θ, sin θ);
      let dg' := semiAdjoint R dg;
      sqrt (det R (dg' ∘ dg))) =
    1
Tactic:
autodiff
State after:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x =>
      let s := -sin x;
      let c := cos x;
      let dg' := semiAdjoint R fun dx => (dx * s, dx * c);
      sqrt ((dg' ∘ fun dx => (dx * s, dx * c)) 1)) =
    1

State before:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x =>
      let s := -sin x;
      let c := cos x;
      let dg' := semiAdjoint R fun dx => (dx * s, dx * c);
      sqrt ((dg' ∘ fun dx => (dx * s, dx * c)) 1)) =
    1
Tactic:
autodiff
State after:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x =>
      let s := -sin x;
      let c := cos x;
      sqrt
        (((fun yz =>
              let x₁ := s * yz.1;
              let x₂ := c * yz.2;
              x₁ + x₂) ∘
            fun dx => (dx * s, dx * c))
          1)) =
    1

State before:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x =>
      let s := -sin x;
      let c := cos x;
      sqrt
        (((fun yz =>
              let x₁ := s * yz.1;
              let x₂ := c * yz.2;
              x₁ + x₂) ∘
            fun dx => (dx * s, dx * c))
          1)) =
    1
Tactic:
simp
State after:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x => sqrt (sin x * sin x + cos x * cos x)) = 1

State before:
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x => sqrt (sin x * sin x + cos x * cos x)) = 1
Tactic:
sorry_proof
State after:
no goals