OAI/Analysis/CircleDomains/Reflection/ReflectionPrincipalSolution.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Solve the actual bounded, compact, reflection-invariant coefficient field. The original coefficient is retained exactly on the circular exterior.

  1. lemma OAI.CircleDomainRigidity.exists_round_invariant_principal_solution line 17
  2. lemma OAI.CircleDomainRigidity.exists_round_invariant_principal_approximation line 42
  3. lemma OAI.CircleDomainRigidity.exists_round_invariant_principal_approximation_with_coefficient line 64