OAI/Analysis/DiskMaximal/Main.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CenteredDiskEndpoint.hasGradient_iff_hasWeakGradient line 57
2. def OAI.CenteredDiskEndpoint.complexPlane line 91

   Source documentation

   The coordinate isometry preserves Euclidean, not max-product, norms.

   def complexPlane : ℂ ≃ₗᵢ[ℝ] Plane := Complex.orthonormalBasisOneI.repr

   Mentions: OAI.CenteredDiskEndpoint.Plane

3. lemma OAI.CenteredDiskEndpoint.integrable_comp_complexPlane line 93
4. lemma OAI.CenteredDiskEndpoint.integrable_comp_complexPlane_symm line 97
5. lemma OAI.CenteredDiskEndpoint.locallyIntegrable_comp_complexPlane line 101
6. lemma OAI.CenteredDiskEndpoint.gradientNorm_comp_complexPlane line 108
7. lemma OAI.CenteredDiskEndpoint.gradientNorm_comp_complexPlane_symm line 113
8. lemma OAI.CenteredDiskEndpoint.maximalComplex_comp_complexPlane line 124

   Source documentation

   Equality of the actual all-real-radius operators, including the normalization and absolute values. This bridge has no regularity assumption on the input.

   lemma maximalComplex_comp_complexPlane (f : Plane → ℝ) (z : ℂ) :
       maximalComplex (fun w => f (complexPlane w)) z=maximal f (complexPlane z) := by
   …

   Mentions: OAI.CenteredDiskEndpoint.Plane, OAI.CenteredDiskEndpoint.complexPlane, OAI.CenteredDiskEndpoint.maximal

9. lemma OAI.CenteredDiskEndpoint.maximalComplexReal_comp_complexPlane line 139
10. theorem OAI.CenteredDiskEndpoint.main_endpoint line 144

    Distinct definitions of this name: ComparatorChallenges/DiskMaximal.lean:56 (same statement text; different proof or body). Qualify references as OAI.CenteredDiskEndpoint.main_endpoint@path.