OAI/Analysis/CircleDomains/Probability/PrincipalDensityStability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Strong L2 stability of the actual principal density under uniformly bounded almost-everywhere coefficient approximation.

  1. lemma OAI.CircleDomainRigidity.schwartz_principal_density_equation line 13
  2. lemma OAI.CircleDomainRigidity.principal_density_strong_convergence line 30