Soccolo

# This Python 3 environment comes with many helpful analytics libraries installed
# It is defined by the kaggle/python Docker image: https://github.com/kaggle/docker-python
# For example, here's several helpful packages to load

# This code can be run at https://www.kaggle.com/cristiancalin/using-logistic-regression-to-predict-rainfall

import numpy as np  #linear algebra
import pandas as pd # data processing, CSV file I/O (e.g. pd.read_csv)
import torch
from tqdm import tqdm

Soccolo

#When treating the Mobius Transformation f(z)=(az+b)/(cz+d) that sends z1 to w1, z2 to w2 and z3 to w3 and create linear equations.
#The governing equations will be of the form a*zi+b-zi*wi*c-wi*d=0. There will be 3 equations with 4 unknowns, so we have an
#undetermined system of equations. We compute the null-space of the matrix using scipy, and then return the vector with first coefficient 
#equal to 1.

from scipy.linalg import null_space
import numpy as np

def Mobius_transform(z1, z2, z3, w1, w2, w3):
    A=np.array([[z1, 1, -z1*w1, -w1], [z2, 1, -z2*w2, -w2], [z3, 1, -z3*w3, -w3]])

Soccolo

import algebra 
import tactic
import data.real.basic
import data.real.sqrt
import algebra.quadratic_discriminant

structure inner_product (V : Type) [add_comm_group V] [vector_space ℝ V] := 
(inner : V → V → ℝ)
(inner_add_left: ∀ x y z : V, inner (x+y) z= inner x z + inner y z)
(inner_smul_left: ∀ x y : V, ∀ a : ℝ, inner(a • x) y=a * inner x y)

Soccolo

import algebra
import algebra.gcd_domain
import tactic
import data.nat.gcd
import data.int.gcd

-- Let G be a group. Prove that, if there exist m and n coprime such that (xy)^m=(yx)^m 
-- and (xy)^n=(yx)^n, then G is commutative.

variables [G : Type] [group G] 

Soccolo

import algebra 
import tactic
import init.data.nat.basic init.data.nat.div init.meta init.algebra.functions

lemma not_injective_pow {M : Type*} [monoid M] [fintype M] (a : M) : ∃ i j : ℕ, i ≠ j ∧ a ^ i = a ^ j :=
begin
  have := not_injective_infinite_fintype (λ i : ℕ, a ^ i),
  rw [function.injective] at this,
  push_neg at this,
  tauto,

Soccolo

--Author: Cristian Calin

--In this file we shall prove Hlawka's Inequality, which states that, for a real vector space, if x, y, z ∈ V,
--|x+y+z|+|x|+|y|+|z| ≥ |x+y| + |y+z| + |x+z|. The proof was taken from the paper
--"Generalizations of the Hlawka's inequality" by Honda et al.

import algebra 
import tactic
import data.real.basic
import algebra.quadratic_discriminant

Soccolo

import algebra
import analysis.normed_space.inner_product
import data.complex.basic
import tactic
import data.complex.is_R_or_C
import analysis.normed_space.basic
import data.real.basic

variables (F: Type) (𝕜 : Type) [is_R_or_C 𝕜] [add_comm_group F] [vector_space 𝕜 F] [c : inner_product_space.core 𝕜 F]
include c

Soccolo

import data.real.basic
import algebra
import tactic
import algebra.quadratic_discriminant
import algebra.ordered_field
import algebra.ordered_group
import algebra.ordered_ring

open classical
local attribute [instance] prop_decidable