fpvandoorn’s gists

fpvandoorn / pi2_error.lean

Last active March 19, 2019 16:26

	import data.real.pi

	set_option profiler true

	set_option timeout 1000000
	namespace real
	-- the following lemma takes about 9 seconds
	lemma pi_gt_31415 : pi > 3.1415 :=
	begin
	refine lt_of_le_of_lt _ (pi_gt_sqrt_two_add_series 6), rw [mul_comm],

fpvandoorn / pi2.lean

Created March 19, 2019 16:33

	import data.real.pi

	set_option profiler true

	namespace real

	lemma sqrt_two_add_series_step_up' {x z : ℝ} {n : ℕ} (y : ℝ) (hz : sqrt_two_add_series y n ≤ z)
	(h : 2 + x ≤ y ^ 2) (h2 : 0 ≤ y) : sqrt_two_add_series x (n+1) ≤ z :=
	begin
	refine le_trans _ hz, rw [sqrt_two_add_series_succ], apply sqrt_two_add_series_monotone_left,

fpvandoorn / cube.lean

Last active May 29, 2019 05:27

cubing a cube

	/-
	Copyright (c) 2019 Floris van Doorn. All rights reserved.
	Released under Apache 2.0 license as described in the file LICENSE.
	Author: Floris van Doorn

	---

	Proof that a cube (in dimension n ≥ 3) cannot be cubed:
	there does not exist a partition of a cube into finitely many smaller cubes (at least two)
	of different sizes.

fpvandoorn / unused.lean

Last active August 13, 2019 02:45

unused arguments

	-- this Git is supposed to be used on branch sanity_check
	-- You have to run the script "scripts/mk_all.sh", and then this file should compile.
	-- The list after each declaration gives all the positions of the unused arguments (starting at 1). E.g. [2] means that the second argument is unused.
	import all

	#sanity_check_mathlib

	-- topology\uniform_space\uniform_embedding.lean
	#print uniformly_extend_exists -- [7]

fpvandoorn / imo2019_4.lean

Last active August 2, 2019 20:27

IMO 2019-4

	import ring_theory.multiplicity algebra.big_operators tactic.default data.rat.basic
	.two_adic_val_fact

	/- two_adic_val_fact.lean is located here:
	https://gist.githubusercontent.com/kbuzzard/4ca88f429bda4744fd038f7471ebfb67/raw/5fa02ec9f5f2b5edf5020cb20c44167a648e0514/two_adic_val_fact.lean
	-/

	universe variables u v

	open finset

fpvandoorn / incorrect_def_lemma.lean

Last active August 13, 2019 03:38

	/- All declarations in mathlib that
	* are a lemma/theorem but construct data
	* are a definition, but define an element of a proposition

	All automatically generated definitions and all instances are filtered out.
	-/

	-- topology\uniform_space\uniform_embedding.lean
	#print uniform_inducing.mk' -- is a def, should be a lemma/theorem

fpvandoorn / lint_log.txt

Created February 3, 2020 21:23

	2020-02-03T19:39:15.8860466Z /- TYPES ARE MISSING INHABITED INSTANCES: -/
	2020-02-03T19:39:15.8860718Z
	2020-02-03T19:39:15.8861155Z -- topology/topological_fiber_bundle.lean
	2020-02-03T19:39:15.8861629Z #print bundle_trivialization /- inhabited instance missing -/
	2020-02-03T19:39:15.8867768Z #print topological_fiber_bundle_core /- inhabited instance missing -/
	2020-02-03T19:39:15.8867878Z
	2020-02-03T19:39:15.8868166Z -- topology/opens.lean
	2020-02-03T19:39:15.8868492Z #print topological_space.nonempty_compacts /- inhabited instance missing -/
	2020-02-03T19:39:15.8868820Z #print topological_space.closeds /- inhabited instance missing -/
	2020-02-03T19:39:15.8868884Z

fpvandoorn / typeclass_stats.lean

Last active December 3, 2020 02:33

prints stats about typeclasses and instances

	import tactic -- all

	open tactic declaration environment native

	meta def pos_line (p : option pos) : string :=
	match p with
	\| some x := to_string x.line
	\| _ := ""
	end

fpvandoorn / lint_out.lean

Created May 22, 2021 19:35

all declarations (including automatically generated ones) that are ill-typed on commit 0e216ce00.

	/- Checking 74465 declarations (plus 74875 automatically generated ones) in mathlib (only in imported files) -/

	/- The `check_type` linter reports: -/
	/- THE STATEMENTS OF THE FOLLOWING DECLARATIONS DO NOT TYPE-CHECK.
	Some definitions in the statement are marked @[irreducible], which means that the statement is now ill-formed. It is likely that these definitions were locally marked @[reducible], and that type-class instances were applied that don't apply when the definitions are @[irreducible].: -/
	-- algebra\category\Mon\adjunctions.lean
	#print adjoin_one.equations._eqn_1 /- The statement doesn't type-check -/
	#print adjoin_zero_map /- The statement doesn't type-check -/
	#print adjoin_zero.equations._eqn_1 /- The statement doesn't type-check -/
	#print adjoin_one_map /- The statement doesn't type-check -/

fpvandoorn / out.txt

Created January 24, 2023 12:36

to additive dictionary of mathlib3

	antitone.const_mul' ← antitone.const_add,
	finset.prod_powerset_insert ← finset.sum_powerset_insert,
	dist_eq_norm_div' ← dist_eq_norm_sub',
	units.is_unit_mul_units ← add_units.is_add_unit_add_add_units,
	Group.filtered_colimits.colimit_has_inv ← AddGroup.filtered_colimits.colimit_has_neg,
	unique_mul.exists_iff_exists_exists_unique ← unique_add.exists_iff_exists_exists_unique,
	subsemigroup.mem_map ← add_subsemigroup.mem_map,
	free_group.norm ← free_add_group.norm,
	finset.prod_ite_index ← finset.sum_ite_index,
	monoid_hom.to_localization_map ← add_monoid_hom.to_localization_map,

Floris van Doorn fpvandoorn