OAI/Geometry/PinnedDistances/ProductFormula.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakPinned.Arithmetic.totallyComplex_of_sq_neg_one line 20
2. lemma OAI.WeakPinned.Arithmetic.log_product_formula line 33
3. def OAI.WeakPinned.Arithmetic.archWeight line 44
4. lemma OAI.WeakPinned.Arithmetic.sum_archWeight line 47
5. lemma OAI.WeakPinned.Arithmetic.archWeight_nonneg line 53
6. lemma OAI.WeakPinned.Arithmetic.finite_nonunit_places line 58

   Source documentation

   The finitely many nonunit places for a given finite list of differences.

   lemma finite_nonunit_places {ι : Type u2} [Finite ι] (z : ι → K)
       (hz : ∀ i, z i ≠ 0) :
       {v : FinitePlace K | ∃ i, v (z i) ≠ 1}.Finite := by
   …

7. lemma OAI.WeakPinned.Arithmetic.raw_fiber_identity line 71

   Source documentation

   Multiplicativity gives the constant depth sum on each nonzero fiber at every absolute value; neither the embeddings nor the field are fixed.

   lemma raw_fiber_identity (v : AbsoluteValue K ℝ) (a b : K) (ha : a ≠ 0) (hb : b ≠ 0) :
       -Real.log (v a) + -Real.log (v b) = -Real.log (v (a * b)) := by
   …

8. lemma OAI.WeakPinned.Arithmetic.paired_coordinate line 78

   Source documentation

   The algebraic inversion identity used both by the unbounded tree argument and the bounded Mobius argument. This is valid in any field.

   lemma paired_coordinate {F : Type u3} [Field F] (a b c d t : F)
       (ha : c ≠ a) (h : (c-a)*(d-b)=t) : d = b + t/(c-a) := by
   …

   Mentions: OAI.WeakPinned.F

9. lemma OAI.WeakPinned.Arithmetic.paired_difference line 85
10. lemma OAI.WeakPinned.Arithmetic.finite_raw_ultra line 93
11. lemma OAI.WeakPinned.Arithmetic.normalized_log_product_formula line 106