Skip to content

[Analysis/MeanInequalities] Fill in API #71

Description

@SnirBroshi
  • Strict versions of HM-GM / Hölder's / Minkowski's
  • NNReal/ENNReal are missing a lot of stuff that Reals have in this file, such as strict AM-GM
  • EReal has nothing in this file, but should probably have AM-GM / HM-GM / Young's / Hölder's / Minkowski's

Figure out what the discrepancies are and fill them in.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions