MajorArcWorkingMean.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The major arcs at the actual common parameter and working length. The only band hypothesis is the geometry of the common final index, which is supplied independently by mrt_working_parameters.

theorem OAI.TwoPointCorrelations.major_arc_actual_working_mean line 16