problem with different types

Stream: new members

[Pietro Lavino]

the goal of my proof is (-(↑n * (↑n)⁻¹.toReal * (↑n)⁻¹.toReal.log) ≤ (↑n).log). where n is introduced in the hypothesis as a natural number, would this be trivial iff I had that n \neq 0? The latter I believe to be easier to prove as n is defined as the number of atoms in a finite partition that covers a measurable space with a probability measure which must imply that the space itself is not empty. When I hover over each term in the goal each seems to be of type \R, is the toReal causing problems? I was also attempting to just show (↑n)⁻¹.toReal = (↑n)⁻¹ and somehow Inv \N would become the goal. Any help would be greatly appreciated

[Eric Wieser]

Could you make a #mwe?

[Pietro Lavino]

import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Data.ENNReal.Real
import Init.Data.Fin.Basic
import Mathlib.Data.Set.Lattice
import Mathlib.Data.Set.Function
import Mathlib.Analysis.SpecialFunctions.Log.Basic
``````
open MeasureTheory
open ENNReal
open Set
open Function
open scoped BigOperators





structure finpart {α : Type*} (m : MeasurableSpace α) (μ : Measure α) [IsProbabilityMeasure μ] (n: ℕ):=
  (f : Fin n → Set α)          -- A function from finite sets of size n to sets of terms in α
  (measurable : ∀ i : Fin n, MeasurableSet (f i))  -- Each set is measurable
  (disjoint : ∀ i j, i ≠ j → μ (f i ∩ f j) = 0)  -- The sets are pairwise disjoint
  (cover : (⋃ i, f i) = Set.univ)  -- The union of all sets covers the entire space

def met_entropy' {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
  (n : ℕ) (fp : finpart m μ n): ℝ :=
-∑ i in Finset.univ,
   (μ (fp.f i)).toReal* Real.log ((μ (fp.f i)).toReal)

theorem max_entropy {α : Type*} {m : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ]
(n : ℕ) (fp : finpart m μ n) :(met_entropy' n fp  ≤ Real.log n) ∧ (met_entropy' n fp = Real.log (n) ↔
∀ i : Fin n, (μ (fp.f i)).toReal=1/n) :=
by
  constructor
  · by_cases h : ∀ i : Fin n, μ (fp.f i)=1/n
    · simp [met_entropy',h]
      rw[← mul_assoc]
      sorry

[Kevin Buzzard]

I get unknown namespace 'MeasureTheory' after deleting the backticks. Does that code work for you?

[Pietro Lavino]

forgot to include some imports as I did no remember whether they were useful: ```
import Mathlib.Analysis.NormedSpace.FiniteDimension

import Mathlib.Analysis.Convolution
import Mathlib.MeasureTheory.Function.Jacobian
import Mathlib.MeasureTheory.Integral.Bochner
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic

[Kevin Buzzard]

      obtain (rfl | hn) := eq_zero_or_pos n
      · simp
      · simp [toReal_inv, mul_inv_cancel <| show (n : ℝ) ≠ 0 by norm_cast; omega]

but I'm not condoning your goal state, I'm just getting you out of trouble :-)

[Pietro Lavino]

thank you!