Theorems · Definition · real analysis
NNReal.agmSequences
NNReal → NNReal → ℕ → NNReal × NNReal
agmSequences x y is the sequence of (geometric, arithmetic) means
converging to the arithmetic-geometric mean starting from x and y.
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 125 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- NNRealstatement and proof · cited by 4,310
- Nat.iterateproof · cited by 740
- NNReal.sqrtproof · cited by 91
Cited by26
Results whose statement or proof uses this declaration.
- NNReal.agmproof · cited by 20
- NNReal.agmSequences_fst_monotonestatement · cited by 5
- NNReal.agm_commproof · cited by 5
- NNReal.agmSequences_zerostatement · cited by 4
- NNReal.agmSequences_snd_antitonestatement · cited by 3
- NNReal.agmSequences_succ'statement and proof · cited by 3
- NNReal.agm_eq_agm_agmSequences_fst_agmSequences_sndstatement and proof · cited by 3
- NNReal.agm_eq_ciSupstatement and proof · cited by 3
- NNReal.bddAbove_range_agmSequences_fststatement and proof · cited by 3
- NNReal.agmSequences_fst_lt_snd_of_nestatement and proof · cited by 2
- NNReal.agmSequences_monotone_and_antitonestatement and proof · cited by 2
- NNReal.agm_le_agmSequences_sndstatement and proof · cited by 2