continuous multilinear maps

Stream: new members

[Matthew Honnor]

Dear all, I am struggling to work with continuous multilinear maps. Sorry for the long block of code below but one of the problems I am having is that when typing the \up symbol in a new file it will not compile so the only way I know how to get it to appear is in the problem I'm trying to solve. I did shorten the code by changing the goal. The new goal is of course in general false but it is the open 'work_on_goal 2' that I am struggling to close at the moment. I have been trying to close it by first using rw help, but this comes up with an error even though the objects appear to be the same. Any help is much appreciated.

import analysis.complex.basic

import logic.is_empty

import topology.algebra.infinite_sum

import order.minimal

import data.nat.lattice

import analysis.analytic.basic

namespace complex

lemma isolated_zeros
 { U : set ℂ } { f : ℂ → ℂ }{ u : ℂ }
  (h : analytic_on ℂ f U)(hu : u ∈ U )(hzero : f u =0) :
  f=0 :=
  begin
    --get the leading term result
    rw analytic_on at h,
    have hnew := h,
    specialize h u hu,
    rw analytic_at at h,
    cases h with p hp,
    rw has_fpower_series_at at hp,
    cases hp with r hpower,
    have hpsumatu := hpower.has_sum,
    have hprpos := hpower.r_pos,
    specialize hpsumatu (emetric.mem_ball_self hprpos),
    have hptsumatu := has_sum.tsum_eq hpsumatu,
    simp at hptsumatu,
    rw hzero at hptsumatu,
    rw tsum_eq_single 0 _ at hptsumatu,
    have hleading := hptsumatu,
    work_on_goal 2 {apply_instance},
    work_on_goal 2 {intros b' hb',
                    have help : (λ (i : fin b'), 0) = 0,
                    tauto,
                    },
  end

Thanks in advance.

[Kevin Buzzard]

    { intros b' hb',
      rw ← zero_lt_iff at hb',
      haveI : nonempty (fin b') := ⟨⟨0, hb'⟩⟩,
      apply continuous_multilinear_map.map_zero, },

works for me, if I've understood what you wanted a proof of. If I've done the wrong thing then maybe strategically put some sorrys in the proof to get it compiling with warnings but not errors, and then explicitly say which sorry you're interested in.