OAI/Probability/SLE/Mass/GreenMassProcessUniqueness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The uniqueness step used to compare canonical mass with its spatial and temporal dilation. Only the positive compact tests of the two Green remainder kernels are required.

  1. lemma OAI.SLEExactGauge.Multipoint.restricted_kernel_mean_le line 23
  2. lemma OAI.SLEExactGauge.Multipoint.positive_mass_process_eq_of_cross_kernel line 29