OAI/Analysis/AffineBernstein/FlatLogEuler.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.flatLogAreaRatio line 17
2. lemma OAI.AffineBernstein.contDiffAt_flatLogAreaRatio line 20
3. lemma OAI.AffineBernstein.flatEulerWeights_exp line 30
4. lemma OAI.AffineBernstein.flatLogAreaRatio_balance line 50
5. lemma OAI.AffineBernstein.matrix_adjugate_entry line 62
6. def OAI.AffineBernstein.flatInverseTrace line 67
7. def OAI.AffineBernstein.flatInversePair line 70
8. theorem OAI.AffineBernstein.flat_log_euler_of_weighted line 74

   Source comment

   Exact logarithmic form of the two-block Euler equation.

   theorem flat_log_euler_of_weighted {W : Set E} (hW : IsOpen W)
       {B : E → Matrix ι ι ℝ} {R : E → Matrix κ κ ℝ}
       (hB : ∀ x ∈ W, ContDiffAt ℝ ∞ (fun y i j => B y i j) x)
       (hR : ∀ x ∈ W, ContDiffAt ℝ ∞ (fun y i j => R y i j) x)
       (hBd : ∀ x ∈ W, 0 < (B x).det) (hRd : ∀ x ∈ W, 0 < (R x).det)
       (v : ι → E) (w : κ → E) {δ c : ℝ} (hc : δ*c = 1-δ)
       (hnz : δ*c ≠ 0) {x : E} (hx : x ∈ W)
       (heuler :
         (∑ j, ∑ i, (B x).adjugate i j * dirDeriv (v j) (dirDeriv (v i) (flatBaseEulerWeight B R δ)) x) +
         (∑ j, ∑ i, (R x).adjugate i j * dirDeriv (w j) (dirDeriv (w i) (flatAngularEulerWeight B R δ)) x) = 0) :
       let t := flatLogAreaRatio B R δ
   …

   Mentions: OAI.AffineBernstein.dirDeriv, OAI.AffineBernstein.flatBaseEulerWeight, OAI.AffineBernstein.flatAngularEulerWeight, OAI.AffineBernstein.flatLogAreaRatio